proposition: Lemma weaksum_r_unique_strong : forall (An : nat -> R) (r1 r2 : R) (Pr1 : Cv_radius_weak An r1) (Pr2 : Cv_radius_weak An r2) (x : R), Rabs x < r1 -> Rabs x < r2 -> weaksum_r An r1 Pr1 x = weaksum_r An r2 Pr2 x.
proof: Proof. intros An r1 r2 Pr1 Pr2 x x_bd1 x_bd2. assert (T1 := weaksum_r_sums _ _ Pr1 _ x_bd1) ; assert (T2 := weaksum_r_sums _ _ Pr2 _ x_bd2) ; eapply Rpser_unique ; eassumption. Qed.
imports: Reals Rinterval Lra Rpser_def Rpser_base_facts Rpser_cv_facts