proposition: Lemma sum_scal_compat : forall (r : R) (rAn' : infinite_cv_radius (r * An)%Rseq), sum (r * An)%Rseq rAn' == ((fun _ => r) * sum An rAn)%F.
proof: Proof. intros r rAn' x. assert (H1 := sum_sums (r * An)%Rseq rAn' x) ; assert (H2 := Rpser_scal_compat r _ _ _ (sum_sums An rAn x)) ; eapply Rpser_unique ; eassumption. Qed.
imports: Reals Lra Rsequence Rseries_def Rseries_cv_facts Rpser_def Rpser_sums Rpser_base_facts Rpser_cv_facts Rpser_radius_facts Rinterval Rfunction_def Rextensionality