proposition: Lemma derivable_pt_lim_in_sum_r: forall An r (rho : finite_cv_radius An r) x, Rball 0 r x -> derivable_pt_lim_in (Rball 0 r) (sum_r An r rho) x (sum_r_derive An r rho x).
proof: Proof. intros ; apply derivable_pt_lim_derivable_pt_lim_in, derivable_pt_lim_sum_r ; erewrite <- Rball_0_simpl ; eassumption. 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