proposition: Lemma sum_r_ext : forall (r : R) (rAn : finite_cv_radius An r) (rBn : finite_cv_radius Bn r), sum_r An r rAn == sum_r Bn r rBn.
proof: Proof. intros r rAn rBn x. unfold sum_r ; destruct (Rlt_le_dec (Rabs x) r) ; trivial ; apply weaksum_r_ext. Qed.
imports: Reals Rsequence_def Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_sums Rpser_cv_facts Rinterval Ranalysis_def Rfunction_facts Tactics