proposition: Lemma Rser_cv_scal_compat_r: forall An la (l : R), Rser_cv An la -> Rser_cv (An * l) (la * l).
proof: Proof. intros ; eapply Rseq_cv_eq_compat. apply Rseq_sum_scal_compat_r. apply Rseq_cv_mult_compat ; intuition. Qed.
imports: Rsequence Rseries_def