proposition: Lemma binomial_sum : forall (x y:C) n, (x + y) ^ n = sum_f_C0 (fun p => IRC (Binomial.C n p) * x ^ p * y ^ (n - p)) n.
proof: Proof. intros x y n. induction n. unfold Binomial.C; simpl. rewrite <- Ceq; simpl; split; field. destruct n. unfold Binomial.C; simpl. rewrite <- Ceq; simpl; split; field. rewrite sum_f_C0_simpl. rewrite <- sum_f_C0_reindex. rewrite Csum_eq_compat with _ (fun k => Binomial.C (S n) k * x ^ S k * y ^ (S (S n) - S k) + Binomial.C (S n) (S k) * x ^ S k * y ^ (S (S n) - S k)) _. rewrite sum_f_C0_add_compat. rewrite Cpow_S. rewrite IHn. rewrite Cmult_add_distr_l. do 2 (rewrite Cmult_comm; rewrite sum_f_C0_mult). assert (AP:forall a b c d e f, a = d + f -> b = c + e -> a + b = c + (d + e) + f) by (intros; subst; ring); apply AP; clear AP. rewrite sum_f_C0_simpl. repeat rewrite binomial_diag. repeat rewrite Nat.sub_diag. apply Cadd_eq_compat. apply Csum_eq_compat_weak; intro; simpl; ring. simpl; ring. rewrite <- sum_f_C0_reindex. apply Cadd_eq_compat. simpl; repeat rewrite binomial_zero; ring. apply Csum_eq_compat; intros j Hj. rewrite (Nat.sub_succ_l _ (S n)); [|lia]. simpl; ring. intros j Hj. repeat rewrite <- Cmult_add_distr_r. rewrite <- Binomial.pascal; [|lia]. rewrite Cadd_IRC_Rplus; trivial. Qed.
imports: Lia Rsequence_def Rsequence_facts Rsequence_cv_facts Rsequence_usual_facts Rtactic MyRIneq Cprop_base Csequence Csequence_facts Cpser_def Cpser_base_facts Cpser_facts Cseries Cseries_facts Cdefinitions Canalysis_def