proposition: Lemma lex_trans : forall (A B : Type) (eq_bool : A -> A -> bool) o1 o2 (eq_bool_ok : forall a1 a2, if eq_bool a1 a2 then a1 = a2 else a1 <> a2), antisymmetric A o1 -> transitive A o1 -> transitive B o2 -> transitive _ (lex eq_bool o1 o2).
proof: Proof. unfold transitive, lex; intros A B eq_bool o1 o2 eq_bool_ok A1 T1 T2 p1 p2 p3; destruct p1 as [a1 b1]; destruct p2 as [a2 b2]; destruct p3 as [a3 b3]. generalize (eq_bool_ok a1 a2); case (eq_bool a1 a2); [intro a1_eq_a2; subst a1 | intro a1_diff_a2]. generalize (eq_bool_ok a2 a3); case (eq_bool a2 a3); [intro a2_eq_a3; subst a2 | intro a2_diff_a3]. apply T2. intros _ a2_t_a3; assumption. generalize (eq_bool_ok a2 a3); case (eq_bool a2 a3); [intro a2_eq_a3; subst a2 | intro a2_diff_a3]. generalize (eq_bool_ok a1 a3); case (eq_bool a1 a3); [intro a1_eq_a3; subst a1 | intro a1_diff_a3]. apply False_rect; apply a1_diff_a2; reflexivity. intros a1_lt_a3 _; assumption. generalize (eq_bool_ok a1 a3); case (eq_bool a1 a3); [intro a1_eq_a3; subst a1 | intro a1_diff_a3]. intros a3_lt_a2 a2_lt_a3; absurd (a3 = a2). assumption. exact ( A1 a3 a2 a3_lt_a2 a2_lt_a3). intros a1_lt_a2 a2_lt_a3; exact (T1 _ _ _ a1_lt_a2 a2_lt_a3). Qed.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)