proposition: Lemma sum_expand_compat : forall l (rAn' : infinite_cv_radius (An_expand An l)), forall x, sum (An_expand An l) rAn' x = sum An rAn (l * x).
proof: Proof. intros l rAn' x ; assert (H1 := sum_sums _ rAn' x) ; assert (H2 := Rpser_expand_compat _ _ _ _ (sum_sums An rAn (l * 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