proposition: Lemma sum_derive_sums : forall (An : nat -> C) (Pr : infinite_cv_radius An) (z : C), Cpser (An_deriv An) z (sum_derive An Pr z).
proof: Proof. intros An Pr z ; unfold sum_derive ; apply weaksum_r_derive_sums ; intuition. Qed.
imports: Rinterval Ranalysis_def Rpser_def Rpser_base_facts Rpser_cv_facts Rpser_sums Rpow_facts Rsequence_def Rsequence_facts Rseries_def Rseries_facts RFsequence_facts Cpow Cpser_def Cpser_base_facts CFsequence CFsequence_facts Csequence Csequence_def Csequence_facts Cmet Cnorm Ctacfield Cprop_base Canalysis_def Canalysis_cont Canalysis_deriv Canalysis_basic_facts