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