proposition: Lemma tot_ext_nat_total r : is_total (fun _ => True) (tot_ext_nat r).
proof: Proof. unfold tot_ext_nat; red; ins. eapply tot_ext_total with (r:=r) (dom := rev (List.seq 0 (S (a + b)))) in NEQ; desf; eauto; rewrite <- in_rev, in_seq; lia. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn