proposition: Lemma sum_unique : forall (An : nat -> R) (Pr1 Pr2 : infinite_cv_radius An) (x : R), sum An Pr1 x = sum An Pr2 x.
proof: Proof. intros An Pr1 Pr2 x ; assert (T1 := sum_sums _ Pr1 x) ; assert (T2 := sum_sums _ Pr2 x) ; eapply Rpser_unique ; eassumption. Qed.
imports: Reals Rinterval Lra Rpser_def Rpser_base_facts Rpser_cv_facts