proposition: Lemma tot_ext_nat_trans r : transitive (tot_ext_nat r).
proof: Proof. unfold tot_ext_nat; red; ins; desf; destruct (le_lt_dec k k0) as [LE|LE]; [|apply Nat.lt_le_incl in LE]; [exists k0|exists k]; eapply tot_ext_trans; eauto; rewrite (seq_split _ LE), rev_app_distr; apply tot_ext_extends_dom; eauto. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn