Provide instances of `LawfulOrd` where `Ord` is used. Find theorems where `Ord` is used and replace them with `LawfulOrd`.