proposition: Lemma sum_sums : forall (An : nat -> R) (Pr : infinite_cv_radius An), forall x, Rpser An x (sum An Pr x).
proof: Proof. intros An Pr x. apply weaksum_r_sums ; intuition (auto with real). Qed.
imports: Reals Rinterval Lra Rpser_def Rpser_base_facts Rpser_cv_facts