proposition: Lemma tot_ext_total A (dom : list A) r : is_total (fun x => In x dom) (tot_ext dom r).
proof: Proof. induction dom; red; ins; desf. eapply one_ext_total_elem in NEQ; desf; eauto. eapply not_eq_sym, one_ext_total_elem in NEQ; desf; eauto. eapply IHdom in NEQ; desf; eapply one_ext_extends in NEQ; eauto. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn