proposition: Lemma one_ext_irr : acyclic r -> irreflexive one_ext.
proof: Proof. red; ins; unfold one_ext in *; desf; eauto using clos_trans_in_rt. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn