proposition: Lemma tot_ext_extends A dom (r : relation A) : r ⊆ tot_ext dom r.
proof: Proof. induction dom; ins; eauto using one_ext_extends with hahn. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn