proposition: Lemma total_order_from_list_trans A (l : list A) (ND: NoDup l) x y z : total_order_from_list l x y -> total_order_from_list l y z -> total_order_from_list l x z.
proof: Proof. unfold total_order_from_list; ins; desf. replace (l0 ++ x :: l4 ++ y :: l5) with ((l0 ++ x :: l4) ++ y :: l5) in H0 by (rewrite <- app_assoc; ins). apply NoDup_eq_simpl in H0; try rewrite <- app_assoc; ins; desf. eexists l0, (_ ++ y :: _), _; rewrite <- app_assoc; ins. Qed.
imports: HahnBase HahnList HahnRelationsBasic