proposition: Lemma tot_ext_extends_dom A dom dom' (r : relation A) : tot_ext dom r ⊆ tot_ext (dom' ++ 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