proposition: Lemma sum_zip_compat : forall rAnBn x, sum (Rseq_zip An Bn) rAnBn x = sum An rAn (x ^ 2) + x * sum Bn rBn (x ^ 2).
proof: Proof. intros rAnBn x ; assert (Ha := sum_sums An rAn (x ^ 2)) ; assert (Hb := sum_sums Bn rBn (x ^ 2)) ; assert (Hab := sum_sums _ rAnBn x) ; 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