proposition: Lemma tot_ext_irr A (dom : list A) r : acyclic r -> irreflexive (tot_ext dom r).
proof: Proof. induction dom; ins. apply one_ext_irr, trans_irr_acyclic; eauto using tot_ext_trans. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn