proposition: Lemma sum_r_zip_compat_0_l : forall An r rAn rAn0 x, Rabs x < r -> Rabs (x ^ 2) < r -> sum_r (Rseq_zip An 0) r rAn0 x = sum_r An r rAn (x ^ 2).
proof: Proof. intros An r rAn rAn0 x x_bd x2_bd ; assert (Ha := sum_r_sums An r rAn (x ^ 2) x2_bd) ; assert (Hab := sum_r_sums _ r rAn0 x x_bd) ; assert (Hab' := Rpser_zip_compat_0_l _ _ _ Ha) ; eapply Rpser_unique ; eassumption. Qed.
imports: MyReals MyINR MyNNR Rsequence_def Rsequence_facts Rsequence_cv_facts Rsequence_sums_facts Rsequence_base_facts Rsequence_rewrite_facts Rsequence_usual_facts Rsequence_subsequence PeanoNat Lra Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_cv_facts Rpser_radius_facts Rpser_sums Rpser_derivative Rpser_derivative_facts Rfunction_def Functions Rextensionality Rpow_facts Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity