proposition: Lemma recurrence a b Afirst Bfirst all Afirst_ahead Bfirst_ahead ahead : 0 < b -> b < a -> (a + b) * Afirst = a * all -> (a + b) * Bfirst = b * all -> Afirst + Bfirst = all -> (a - 1 + b) * Afirst_ahead = (a - b - 1) * Afirst -> (a - 1 + b) * Bfirst_ahead = (a - (b - 1)) * Bfirst -> Afirst_ahead + Bfirst_ahead = ahead -> (a + b) * ahead = (a - b) * all.
proof: Proof. destruct a. intros ? ?; exfalso; lia. destruct b. inversion 1. simpl (S a - 1). simpl (S b - 1). replace (S a - S b - 1) with (a - S b) by lia. replace (b - 0) with b by lia. replace (a - 0) with a by lia. intros _ L HA HB <- IHA IHB <-. apply Nat.mul_cancel_l with (p := (a + S b)). lia. match goal with |- ?x * (?y * ?z) = _ => transitivity (y * (x * z)) end. ring. rewrite Nat.mul_add_distr_l. rewrite IHA, IHB. rewrite Nat.mul_add_distr_l. match goal with |- ?x * (?y * ?z) + ?x' * (?y' * ?z') = _ => transitivity (y * (x * z) + y' * (x' * z')) end. ring. rewrite HA, HB. match goal with |- ?x * (?y * ?z) + ?x' * (?y' * ?z) = _ => transitivity ((x * y + x' * y') * z) end. ring. rewrite Nat.mul_assoc. f_equal. replace (S a - S b) with (a - b) by lia. replace (S a - b) with (1 + (a - b)) by lia. replace (a - S b) with (a - b - 1) by lia. replace a with (b + 1 + (a - b - 1)) by lia. generalize (a - b - 1); intros c. replace (b + 1 + c - b - 1) with c by lia. replace (b + 1 + c - b) with (c + 1) by lia. ring. Qed.
imports: Arith ZArith String List Psatz Factorial