proposition: Theorem exp_Pascal : forall a b n : nat, power (a + b) n = sum_nm 0 n (fun k : nat => binomial n k * (power a (n - k) * power b k)).
proof: Proof. simple induction n; auto; clear n. intros n; case n; clear n. simpl in |- *; intros; ring. intros n H'. apply trans_equal with (y := (a + b) * power (a + b) (S n)). simpl in |- *; auto. rewrite H'; rewrite Nat.mul_add_distr_r; repeat rewrite sum_nm_times. rewrite sum_nm_i; rewrite binomial_def1. replace (1 * (power a (S n - 0) * power b 0)) with (power a (S n)); [ idtac | simpl in |- *; ring ]; auto. rewrite sum_nm_f; rewrite binomial_def3. replace (S n - (0 + S n)) with 0; [ idtac | simpl in |- *; rewrite Nat.sub_diag]; auto. replace (power a 0) with 1; auto. replace (b * (1 * (1 * power b (0 + S n)))) with (b * power b (S n)); [ idtac | simpl in |- *; ring ]; auto. rewrite (t_sum_Svars 0 n). replace (a * power a (S n) + sum_nm 1 n (fun z : nat => a * (binomial (S n) z * (power a (S n - z) * power b z))) + (sum_nm 1 n (fun x : nat => b * (binomial (S n) (pred x) * (power a (S n - pred x) * power b (pred x)))) + b * power b (S n))) with (power a (S (S n)) + (sum_nm 1 n (fun x : nat => binomial (S (S n)) x * (power a (S (S n) - x) * power b x)) + power b (S (S n)))). rewrite (sum_nm_i (S n) 0). rewrite (sum_nm_f 1 n). rewrite binomial_def1; rewrite binomial_def3. replace (S (S n) - 0) with (S (S n)); auto. replace (S (S n) - (1 + S n)) with 0; auto with arith. replace (power a 0) with 1; auto. replace (power b 0) with 1; auto. replace (1 * (power a (S (S n)) * 1)) with (power a (S (S n))); [ idtac | simpl in |- *; ring ]; auto. replace (1 + S n) with (S (S n)); auto. replace (1 * (1 * power b (S (S n)))) with (power b (S (S n))); [ idtac | simpl in |- *; ring ]; auto. repeat rewrite <- Nat.add_assoc; apply f_equal2 with (f := plus); auto. repeat rewrite Nat.add_assoc; apply f_equal2 with (f := plus); auto. rewrite sum_nm_add. apply sum_nm_ext. intros x H'0. replace (pred (1 + x)) with x; [ idtac | auto ]. replace (S (S n) - (1 + x)) with (S n - x); [ idtac | auto ]. replace (S n - (1 + x)) with (n - x); [ idtac | auto ]. replace (1 + x) with (S x); [ idtac | auto ]. rewrite (binomial_def4 (S n)); auto with arith. rewrite Nat.sub_succ_l; simpl in |- *; auto; try ring. Qed.
imports: Coq(Arith ArithRing Wf_nat)