proposition: Lemma reduce_lt_plus: forall a b c: T1, lt (a+ b) (a + c) <-> lt b c.
proof: Proof. induction a. 1: easy. simpl. split; intro H; destruct b, c. - exfalso. now apply lt_irrefl in H. - apply zero_lt. - exfalso. compare destruct a1 b1 as Hcomp. + apply lt_inv_coeff in H. lia. + apply lt_inv_head in H. now apply lt_not_ge in Hcomp. + now apply lt_inv_tail, lt_plus_r in H. - compare destruct a1 b1 as Hcomp_b1; compare destruct a1 c1 as Hcomp_c1. + apply lt_inv_coeff_dec in H as [Hlt | (Heq, Hlt)]. * apply coeff_lt; lia. * apply PeanoNat.Nat.succ_inj, PeanoNat.Nat.add_cancel_l in Heq as ->. now apply tail_lt. + now apply head_lt. + now apply lt_inv_coeff in H; lia. + now apply lt_inv_head, le_not_gt in H. + assumption. + now apply lt_inv_head, le_not_gt in H. + now apply head_lt. + apply head_lt. now apply (@lt_trans b1 a1 c1) in Hcomp_c1. + now apply lt_inv_tail, (IHa2 (cons b1 n0 b2) (cons c1 n1 c2)) in H. - now apply not_lt_zero in H. - compare destruct a1 c1 as Hcomp_c1. + apply coeff_lt; lia. + now apply head_lt. + apply tail_lt, lt_plus_l. - now apply not_lt_zero in H. - compare destruct a1 b1 as Hcomp_b1; compare destruct a1 c1 as Hcomp_c1. + apply lt_inv_coeff_dec in H as [Hlt | (Heq, Hlt)]. * apply coeff_lt; lia. * rewrite Heq. now apply tail_lt. + now apply head_lt. + now apply lt_inv_head, le_not_gt in H. + now apply lt_inv_head, le_not_gt in H. + assumption. + apply lt_inv_head, le_not_gt in H. now apply (@lt_trans c1 a1 b1) in Hcomp_b1. + apply coeff_lt; lia. + now apply head_lt. + now apply tail_lt, IHa2. 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)