proposition: Lemma Rser_cv_opp_compat: forall An l, Rser_cv An l -> Rser_cv (- An) (- l).
proof: Proof. intros ; eapply Rseq_cv_eq_compat. apply Rseq_sum_opp_compat. apply Rseq_cv_opp_compat ; assumption. Qed.
imports: Rsequence Rseries_def