proposition: Lemma Rser_cv_shifts : forall k An l, Rser_cv An l -> Rser_cv (Rseq_shifts An (S k)) (l - Rseq_sum An k).
proof: Proof. intros k An l Hl ; eapply Rseq_cv_eq_compat. intro n ; apply Rseq_sum_shifts_compat. apply Rseq_cv_minus_compat. apply Rseq_cv_shifts_compat_reciprocal ; assumption. apply Rseq_constant_cv. Qed.
imports: Rsequence Rseries_def