proposition: Lemma Rpser_partial_sum_derive_pt_lim_in: forall c r An n x, derivable_pt_lim_in (Rball c r) (fun x => Rseq_pps An x n) x (Rpser_partial_sum_derive An n x).
proof: Proof. intros ; apply derivable_pt_lim_derivable_pt_lim_in, Rpser_partial_sum_derive_pt_lim. 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