proposition: Lemma lex_trans : forall (A B : Set) eq_A_dec o1 o2, antisymmetric A o1 -> transitive A o1 -> transitive B o2 -> transitive _ (lex _ _ eq_A_dec o1 o2).
proof: Proof. unfold transitive, lex; intros A B eq_A_dec o1 o2 A1 T1 T2 p1 p2 p3; destruct p1 as [a1 b1]; destruct p2 as [a2 b2]; destruct p3 as [a3 b3]; elim (eq_A_dec a1 a2); intro eq1. subst a2; elim (eq_A_dec a1 a3); intro eq2; trivial; apply T2. intro lt1; elim (eq_A_dec a1 a3); intro eq3. subst a3; elim (eq_A_dec a2 a1); intro eq2. subst a2; absurd (a1=a1); trivial. intro lt2; generalize (A1 _ _ lt1 lt2); contradiction. elim (eq_A_dec a2 a3); intro eq4. subst a3; trivial. intro lt2; apply T1 with a2; trivial. Qed.
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term