proposition: Lemma sum_r_sums : forall (An : nat -> R) (r : R) (Pr : finite_cv_radius An r), forall x, Rabs x < r -> Rpser An x (sum_r An r Pr x).
proof: Proof. intros An r Pr x x_ub. unfold sum_r ; destruct (Rlt_le_dec (Rabs x) r) as [x_bd | x_nbd]. apply weaksum_r_sums. apply (proj1 (middle_is_in_the_middle _ _ x_bd)). apply False_ind ; lra. Qed.
imports: Reals Rinterval Lra Rpser_def Rpser_base_facts Rpser_cv_facts