proposition: Lemma sum_r_alt_compat : forall rAn', sum_r (Rseq_alt An) r rAn' x = sum_r An r rAn (- x).
proof: Proof. intro rAn' ; assert (x_bd' : Rabs (- x) < r) by (rewrite Rabs_Ropp ; assumption) ; assert (Ha := sum_r_sums An r rAn _ x_bd') ; assert (Ha' := sum_r_sums _ r rAn' _ x_bd) ; assert (Ha'' := Rpser_alt_compat _ _ _ Ha) ; 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