proposition: Lemma total_order_from_list_insert : forall A (l1: list A) a l2 x y, total_order_from_list (l1 ++ l2) x y -> total_order_from_list (l1 ++ a :: l2) x y.
proof: Proof. ins; rewrite total_order_from_list_app, total_order_from_list_cons in *; ins; desf; eauto. Qed.
imports: HahnBase HahnList HahnRelationsBasic