proposition: Lemma Rpser_prod_compat: forall An Bn x la la' lb, Rpser An x la -> Rpser_abs An x la' -> Rpser Bn x lb -> Rpser (An # Bn) x (la * lb).
proof: Proof. intros An Bn x la la' lb Ha Ha' Hb. eapply Rseq_cv_eq_compat ; [apply Rseq_pps_prod_unfold |]. eapply Rser_cv_prod_compat ; 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