proposition: Lemma sum_r_zip_compat : forall rAnBn, Rabs (x ^ 2) < r -> sum_r (Rseq_zip An Bn) r rAnBn x = sum_r An r rAn (x ^ 2) + x * sum_r Bn r rBn (x ^ 2).
proof: Proof. intros rAnBn x_bd' ; assert (Ha := sum_r_sums An r rAn (x ^ 2) x_bd') ; assert (Hb := sum_r_sums Bn r rBn (x ^ 2) x_bd') ; assert (Hab := sum_r_sums _ r rAnBn x x_bd) ; assert (Hab' := Rpser_zip_compat _ _ _ _ _ Ha Hb). 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