proposition: Lemma sum_r_unfold : forall An r r' (pr1 : finite_cv_radius An r) (pr2 : Cv_radius_weak An r') x, Rabs x < r -> Rabs x < r' -> sum_r An r pr1 x = weaksum_r An r' pr2 x.
proof: Proof. intros An r r' pr1 pr2 x x_bd x_bd' ; unfold sum_r ; destruct (Rlt_le_dec (Rabs x) r) as [H1 | Hf] ; [| exfalso ; lra]. apply weaksum_r_unique_strong ; [apply middle_is_in_the_middle |] ; 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