proposition: Lemma L0 : forall p, P p.
proof: Proof. apply well_founded_induction with LT. { apply T1_wf. } intros b Hind; unfold P. intros a c Hnf_a Hnf_b Hnf_c. destruct b, c. 3:now rewrite !mult_a_0, !plus_zero_r. 1-2:now rewrite !plus_zero, !mult_a_0. rewrite plus_cons_cons_eqn. destruct a. 1: now rewrite mult_0_a. compare destruct b1 c1 as Hcomp_b1_c1; destruct b1, a1; try destruct c1; simpl. 5,7,9,11,13-16: now apply not_lt_zero in Hcomp_b1_c1. - f_equal; lia. - rewrite compare_cons. rewrite Nat.compare_refl, !compare_refl. f_equal; lia. - rewrite compare_cons. now rewrite Nat.compare_refl, !compare_refl. - rewrite compare_refl. now destruct (compare a1_1 b1_1). - reflexivity. - compare destruct a1_1 c1_1 as Hcomp_a11_c11. + rewrite compare_cons. rewrite compare_refl. enough (Nat.compare n2 (S (n2 + n3)) = Lt) as -> by reflexivity. apply Nat.compare_lt_iff; lia. + rewrite compare_cons. now apply compare_lt_iff in Hcomp_a11_c11 as ->. + rewrite compare_cons. rewrite compare_refl, Nat.compare_refl. eenough (compare a1_2 (a1_2 + _) = Lt) as -> by reflexivity. apply compare_lt_iff, lt_plus_l. - apply lt_inv_strong in Hcomp_b1_c1 as [Hlt | Heqa Hlt | Heqa Heqn Hlt]. + rewrite compare_cons. now apply compare_lt_iff in Hlt as ->. + rewrite compare_cons. rewrite Heqa, compare_refl. now apply Nat.compare_lt_iff in Hlt as ->. + rewrite compare_cons. rewrite Heqa, Heqn, compare_refl, Nat.compare_refl. now apply compare_lt_iff in Hlt as ->. - compare destruct a1_1 c1_1 as Hcomp_a11_c11. + apply lt_inv_strong in Hcomp_b1_c1 as [Hlt | Heqa Hlt | Heqa Heqn Hlt]. * apply compare_gt_iff in Hlt as ->. eenough (compare (cons a1_1 n3 _) (cons a1_1 (S (n3 + _)) _) = Lt) as -> by reflexivity. apply compare_lt_iff, coeff_lt; lia. * rewrite Heqa, compare_refl. eenough (compare (cons a1_1 (S(n3 + n2)) _) (cons a1_1 (S(n3 + n4)) _) = Lt) as -> by reflexivity. apply compare_lt_iff, coeff_lt. lia. * rewrite Heqa, Heqn, compare_refl. eenough (compare (cons a1_1 (S (n3 + n4)) b1_2) (cons a1_1 (S (n3 + n4)) c1_2) = Lt) as -> by reflexivity. now apply compare_lt_iff, tail_lt. + compare destruct a1_1 b1_1 as Hcomp_a11_b11. * eenough (compare (cons a1_1 _ _) (cons c1_1 _ _) = Lt) as -> by reflexivity. now apply compare_lt_iff, head_lt. * now apply compare_lt_iff in Hcomp_b1_c1 as ->. * eenough (compare (cons a1_1 _ _) (cons c1_1 _ _) = Lt) as -> by reflexivity. now apply compare_lt_iff, head_lt. + apply lt_inv_strong in Hcomp_b1_c1 as [Hlt | Heqa Hlt | Heqa Heqn Hlt]. * apply (@lt_trans b1_1 c1_1 a1_1), compare_gt_iff in Hcomp_a11_c11 as ->; auto. eenough (compare (cons a1_1 n3 (a1_2 + cons b1_1 _ _)) (cons a1_1 n3 (a1_2 + cons c1_1 _ _)) = Lt) as -> by reflexivity. now apply compare_lt_iff, tail_lt, reduce_lt_plus, head_lt. * subst. apply compare_gt_iff in Hcomp_a11_c11 as ->. eenough (compare (cons a1_1 n3 (a1_2 + cons c1_1 n2 _)) (cons a1_1 n3 (a1_2 + cons c1_1 n4 _)) = Lt) as -> by reflexivity. now apply compare_lt_iff, tail_lt, reduce_lt_plus, coeff_lt. * subst. apply compare_gt_iff in Hcomp_a11_c11 as ->. enough (compare (cons a1_1 n3 (a1_2 + cons c1_1 n4 b1_2)) (cons a1_1 n3 (a1_2 + cons c1_1 n4 c1_2)) = Lt) as -> by reflexivity. now apply compare_lt_iff, tail_lt, reduce_lt_plus, tail_lt. - rewrite_ind Hind b2. - rewrite_ind Hind b2. apply lt_inv_strong in Hcomp_b1_c1 as [Hlt | Heqa Hlt | Heqa Heqn Hlt]. + rewrite compare_cons. now apply compare_gt_iff in Hlt as ->. + rewrite compare_cons. rewrite Heqa, compare_refl. now apply Nat.compare_gt_iff in Hlt as ->. + rewrite compare_cons. rewrite Heqa, Heqn, compare_refl, Nat.compare_refl. now apply compare_gt_iff in Hlt as ->. - rewrite_ind Hind b2. compare destruct a1_1 b1_1 as Hcomp_a11_b11. + eenough (compare (cons a1_1 (S (n3 + n2)) _) (cons a1_1 n3 _) = Gt) as -> by reflexivity. apply compare_gt_iff, coeff_lt; lia. + eenough (compare (cons b1_1 _ _) (cons a1_1 _ _) = Gt) as -> by reflexivity. now apply compare_gt_iff, head_lt. + eenough (compare (cons a1_1 n3 (a1_2 + _)) (cons a1_1 n3 a1_2) = Gt) as -> by reflexivity. apply compare_gt_iff, tail_lt, lt_plus_l. - rewrite_ind Hind b2; simpl. compare destruct a1_1 b1_1 as Hcomp_ab; compare destruct a1_1 c1_1 as Hcomp_ac. + eenough (compare (cons a1_1 (S (n3 + n2)) _) (cons a1_1 (S (n3 + n4)) _) = Gt) as -> by reflexivity. { apply compare_gt_iff. apply lt_inv_coeff_dec in Hcomp_b1_c1 as [Hlt | (Heq, Hlt)]. - apply coeff_lt; lia. - subst; now apply tail_lt. } + now apply lt_inv_head, le_not_gt in Hcomp_b1_c1. + eenough (compare (cons a1_1 (S (n3 + _)) _) (cons a1_1 n3 _) = Gt) as -> by reflexivity. apply compare_gt_iff, coeff_lt; lia. + eenough (compare (cons b1_1 _ _) (cons a1_1 _ _) = Gt) as -> by reflexivity. now apply compare_gt_iff, head_lt. + now apply compare_gt_iff in Hcomp_b1_c1 as ->. + eenough (compare (cons b1_1 _ _) (cons a1_1 _ _) = Gt) as -> by reflexivity. now apply compare_gt_iff, head_lt. + now apply lt_inv_head, le_not_gt in Hcomp_b1_c1. + exfalso. apply lt_inv_head, le_not_gt in Hcomp_b1_c1. now apply (@lt_trans b1_1 a1_1 c1_1) in Hcomp_ac as Hbc. + enough (compare (cons a1_1 n3 (a1_2 + cons b1_1 n2 b1_2)) (cons a1_1 n3 (a1_2 + cons c1_1 n4 c1_2)) = Gt) as -> by reflexivity. now apply compare_gt_iff, tail_lt, reduce_lt_plus. all: eauto with T1. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)