proposition: Lemma tot_ext_nat_extends2 r : r⁺ ⊆ tot_ext_nat r.
proof: Proof. eauto using tot_ext_nat_extends, tot_ext_nat_trans with hahn. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn