proposition: Lemma Cexp_add : forall a b, Cexp (a + b) = (Cexp a * Cexp b)%C.
proof: Proof. intros a b. unfold Cexp. pose (gt_pser exp_seq) as tg. apply Cser_cv_unique with (tg (a + b)). apply sum_sums. destruct (Cexp_abs_cv a) as [lna Hlna]. eapply Cser_cv_eq_compat. 2:eapply (Ccauchy_product (tg a) (tg b)) ; try apply sum_sums. intro n; simpl. unfold tg, exp_seq ; unfold_gt. rewrite binomial_sum. rewrite sum_f_C0_mult. apply Csum_eq_compat_weak; intros p. unfold Binomial.C. rewrite Cdiv_IRC_Rdiv. repeat rewrite Cmult_IRC_Rmult. repeat rewrite IRC_INR_INC. field; repeat split; replace C0 with (INC O)%C by trivial; apply not_INC; apply fact_neq_0. apply Rmult_integral_contrapositive. INR_solve; apply fact_neq_0. apply Hlna. 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