proposition: Lemma Rser_cv_plus_compat: forall An Bn la lb, Rser_cv An la -> Rser_cv Bn lb -> Rser_cv (An + Bn) (la + lb).
proof: Proof. intros ; eapply Rseq_cv_eq_compat. apply Rseq_sum_plus_compat. apply Rseq_cv_plus_compat ; assumption. Qed.
imports: Rsequence Rseries_def