This commit also adds a lemma relating is_strict_weak_order and total_preorder.
to_unfold
simplify
simp*