proposition: Lemma one_ext_trans : transitive one_ext.
proof: Proof. red; ins; unfold one_ext in *; desf; desf; intuition eauto using clos_trans_in_rt, t_trans, rt_trans. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn