proposition: Lemma sum_alt_compat : forall rAn' x, sum (Rseq_alt An) rAn' x = sum An rAn (- x).
proof: Proof. intros rAn' x ; assert (Ha := sum_sums An rAn (- x)) ; assert (Ha' := sum_sums _ rAn' x) ; 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