proposition: Lemma sum_unfold : forall An r (pr1 : infinite_cv_radius An) (pr2 : Cv_radius_weak An r) x, Rabs x < r -> sum An pr1 x = weaksum_r An r pr2 x.
proof: Proof. intros An r pr1 pr2 x x_ub ; unfold sum ; apply weaksum_r_unique_strong ; [lra | assumption]. Qed.
imports: Reals Lra Rsequence Rseries_def Rseries_cv_facts Rpser_def Rpser_sums Rpser_base_facts Rpser_cv_facts Rpser_radius_facts Rinterval Rfunction_def Rextensionality