proposition: Lemma Cexp_eq_Deriv_Cexp : forall z, Cexp z = Deriv_Cexp z.
proof: Proof. intro z. assert (T1 := sum_sums _ exp_infinite_cv_radius z) ; assert (T2 := sum_derive_sums _ exp_infinite_cv_radius z). symmetry ; eapply Cpser_unique_extentionality. apply Deriv_exp_seq_simpl. apply T2. apply T1. 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