proposition: Lemma tot_ex X (mo : relation X) dom (TOT: is_total dom mo) a b (INa: dom a) (INb: dom b) (NMO: ~ mo a b) (NEQ: a <> b) : mo b a.
proof: Proof. eapply TOT in NEQ; desf; eauto. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets