proposition: Lemma sum_r_expand_compat : forall l (rAn' : finite_cv_radius (An_expand An l) r), Rabs (l * x) < r -> sum_r (An_expand An l) r rAn' x = sum_r An r rAn (l * x).
proof: Proof. intros l rAn' xl_bd ; assert (H1 := sum_r_sums _ _ rAn' x x_bd) ; assert (H2 := Rpser_expand_compat _ _ _ _ (sum_r_sums _ _ rAn (l * x) xl_bd)) ; 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