proposition: Lemma tot_ext_nat_irr r : acyclic r -> irreflexive (tot_ext_nat r).
proof: Proof. red; unfold tot_ext_nat; ins; desf; eapply tot_ext_irr; eauto. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn