proposition: Lemma sum_ext : forall (rAn : infinite_cv_radius An) (rBn : infinite_cv_radius Bn), sum An rAn == sum Bn rBn.
proof: Proof. intros rAn rBn x ; unfold sum ; 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