proposition: Theorem Nnewton : forall n a b, (a + b) ^ n = Nnewton_sum n a b.
proof: Proof. induction n. compute. reflexivity. intros. rewrite Npower_succ. rewrite Nat.mul_add_distr_r. rewrite IHn. unfold Nnewton_sum. rewrite Nfinite_sum_mult_distrib. assert (forall k, a * (Nbinomial n k * a ^ k * b ^ (n - k))= (Nbinomial n k * a ^ (S k) * b ^ (n - k))). intro. assert (a * (Nbinomial n k * a ^ k * b ^ (n - k)) = Nbinomial n k * (a * a ^ k) * b ^ (n - k)). ring. rewrite H. rewrite Npower_succ. reflexivity. assert (Nfinite_sum_0_n n (fun k : nat => a * (Nbinomial n k * a ^ k * b ^ (n - k))) = Nfinite_sum_0_n n (fun k : nat => (Nbinomial n k * a ^(S k) * b ^ (n - k)))). apply Nfinite_sum_eq_compat. exact H. rewrite H0. clear H0. rewrite Nfinite_sum_mult_distrib. assert (forall k:nat, b * (Nbinomial n k * a ^ k * b ^ (n - k)) = Nbinomial n k * a ^ k * b ^ (S (n - k))). intro. assert (b * (Nbinomial n k * a ^ k * b ^ (n - k)) = Nbinomial n k * (a ^ k) * (b * b ^ (n - k))). ring. rewrite H0. rewrite Npower_succ. reflexivity. assert (Nfinite_sum_0_n n (fun k : nat => b * (Nbinomial n k * a ^ k * b ^ (n - k))) = Nfinite_sum_0_n n (fun k : nat => (Nbinomial n k * a ^k)* b ^ (S (n - k)))). apply Nfinite_sum_eq_compat. exact H0. rewrite H1. clear H1. clear H0. clear H. clear IHn. rewrite Nfinite_sum_split_lower. simpl. rewrite Nat.add_0_r. assert (Nfinite_sum_0_n n (fun k : nat => Nbinomial (S n) (S k) * a ^ S k * b ^ (n - k)) = Nfinite_sum_0_n n (fun k : nat => Nbinomial n (S k) * a ^ S k * b ^ (n - k) + Nbinomial n k * a ^ S k * b ^ (n - k))). apply Nfinite_sum_subtle_eq_compat. intros. rewrite <- Nbinomial_pascal. ring. exact H. simpl in H. rewrite H. clear H. rewrite <- Nfinite_sum_plus_compat. assert (b ^ S n + Nfinite_sum_0_n n (fun k : nat => Nbinomial n (S k) * a ^ S k * b ^ (n - k)) = Nfinite_sum_0_n (S n) (fun k : nat => Nbinomial n k * a ^ k * b ^ (S (n - k)))). rewrite Nfinite_sum_split_lower. rewrite Nbinomial_0. simpl. rewrite Nat.sub_0_r. rewrite Nat.add_0_r. assert (Nfinite_sum_0_n n (fun k : nat => Nbinomial n (S k) * a ^ S k * b ^ (n - k)) = Nfinite_sum_0_n n (fun k : nat => Nbinomial n (S k) * a ^ S k * b ^ S (n - S k))). apply Nfinite_sum_subtle_eq_compat. intros. apply le_le_S_eq in H. destruct H. intros. assert (S(n-S k)=n-k). induction n. apply Nat.nle_succ_0 in H. contradiction. apply le_le_S_eq in H. destruct H. rewrite Nat.sub_succ_l. rewrite IHn. symmetry. apply Nat.sub_succ_l. apply le_S_n. auto with arith. apply le_S_n. auto with arith. apply le_S_n. auto with arith. apply eq_eq_nat in H. unfold eq_nat in H. apply eq_nat_eq in H. rewrite H. rewrite Nat.sub_diag. rewrite Nat.sub_succ_l. rewrite Nat.sub_diag. reflexivity. auto with arith. rewrite H0. reflexivity. rewrite H. rewrite Nbinomial_outside. simpl. reflexivity. auto with arith. simpl in H. rewrite H. clear H. reflexivity. assert (b ^ S n + (Nfinite_sum_0_n n (fun k : nat => Nbinomial n (S k) * a ^ S k * b ^ (n - k)) + Nfinite_sum_0_n n (fun k : nat => Nbinomial n k * a ^ S k * b ^ (n - k))) = (b ^ S n + Nfinite_sum_0_n n (fun k : nat => Nbinomial n (S k) * a ^ S k * b ^ (n - k)) + (Nfinite_sum_0_n n (fun k : nat => Nbinomial n k * a ^ S k * b ^ (n - k))))). rewrite Nat.add_assoc. auto with arith. simpl in H0, H. rewrite H0. clear H0. rewrite H. clear H. assert (Nfinite_sum_0_n n (fun k : nat => Nbinomial n k * a ^ k * b ^ S (n - k)) = Nfinite_sum_0_n (S n) (fun k : nat => Nbinomial n k * a ^ k * b ^ S (n - k))). rewrite Nfinite_sum_split_upper. rewrite Nbinomial_outside. simpl. auto with arith. auto with arith. rewrite Nbinomial_outside; auto. ring. Qed.
imports: Arith Compare Nbinomial Ndiv Npow Nfinite_sum