proposition: Lemma one_ext_total_elem : forall x, x <> elem -> one_ext elem x \/ one_ext x elem.
proof: Proof. unfold one_ext; ins; rewrite !clos_refl_transE; tauto. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn