proposition: Lemma total_order_from_list_in1 A (l: list A) x y : total_order_from_list l x y -> In x l.
proof: Proof. unfold total_order_from_list; ins; desf. eauto 10 using in_or_app, in_eq, in_cons. Qed.
imports: HahnBase HahnList HahnRelationsBasic