proposition: Lemma derive_pt_sum : forall (An : Rseq) (rAn : infinite_cv_radius An) (rdAn : infinite_cv_radius (An_deriv An)) x (dAn : derivable_pt (sum An rAn) x), derive_pt (sum An rAn) x dAn = sum (An_deriv An) rdAn x.
proof: Proof. intros ; rewrite derive_pt_eq. replace (sum (An_deriv An) rdAn x) with (sum_derive An rAn x). apply derivable_pt_lim_sum. apply sum_unique. Qed.
imports: Reals Rpow_facts Rfunction_def Rinterval Rextensionality Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Lra MyRIneq Rsequence_facts Rsequence_sums_facts RFsequence RFsequence_facts Rpser_def Rpser_base_facts Rpser_radius_facts Rpser_sums Rpser_sums_facts Tactics