proposition: Lemma Rser_cv_minus_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_minus_compat. apply Rseq_cv_minus_compat ; assumption. Qed.
imports: Rsequence Rseries_def