proposition: Lemma tot_ext_trans A dom (r : relation A) : transitive (tot_ext dom r).
proof: Proof. induction dom; ins; vauto; apply one_ext_trans. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn