proposition: Lemma Rser_cv_shift : forall An l, Rser_cv An l -> Rser_cv (Rseq_shift An) (l - (An O)).
proof: Proof. intros An l Hl ; eapply Rseq_cv_eq_compat. intro n ; apply Rseq_sum_shift_compat. apply Rseq_cv_minus_compat. apply Rseq_cv_shift_compat_reciprocal ; assumption. apply Rseq_constant_cv. Qed.
imports: Rsequence Rseries_def