proposition: Lemma total_order_from_list_cons : forall A (a : A) l x y, total_order_from_list (a :: l) x y <-> a = x /\ In y l \/ total_order_from_list l x y.
proof: Proof. unfold total_order_from_list; split; ins; desf. by destruct l1; ins; desf; eauto using in_or_app, in_eq, in_cons. apply in_split in H0; desf; exists nil; ins; eauto. exists (a :: l1); ins; eauto. Qed.
imports: HahnBase HahnList HahnRelationsBasic