proposition: Lemma sum_mult_compat: forall (rAnBn: infinite_cv_radius (An # Bn)), sum (An # Bn) rAnBn == (sum An rAn * sum Bn rBn)%F.
proof: Proof. intros rAnBn x ; destruct (Rpser_abs_infinite_cv_radius _ rAn x) as [l Ha']. assert (Ha := sum_sums _ rAn x) ; assert (Hb := sum_sums _ rBn x) ; assert (Hab := Rpser_prod_compat _ _ _ _ _ _ Ha Ha' Hb) ; assert (Hab' := sum_sums _ rAnBn x) ; 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