proposition: Lemma D_infty_Rpser : forall (An : Rseq) (Rho : infinite_cv_radius An), D_infty (sum An Rho).
proof: Proof. intros An rho n ; revert rho ; revert An ; induction n ; intros An Rho. constructor. apply D_S with (derivable_sum An Rho) ; apply D_ext with (sum_derive An Rho). intro x ; symmetry ; apply derive_pt_eq_0 ; apply derivable_pt_lim_sum. apply IHn. Qed.
imports: Reals Rsequence_def Rfunction_facts Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Rfunction_classes_def Rfunction_classes_facts Rextensionality Rpser_def Rpser_def Rpser_cv_facts Rpser_sums Rpser_sums_facts Rpser_derivative