proposition: Lemma Rser_cv_shift_rev : forall An l, Rser_cv (Rseq_shift An) l -> Rser_cv An (l + An 0%nat).
proof: Proof. intros An l Hl ; apply Rseq_cv_shift_compat ; apply Rseq_cv_eq_compat with (Rseq_plus (Rseq_sum (Rseq_shift An)) (An O)). intro n ; unfold Rseq_plus, Rseq_constant ; rewrite (Rseq_sum_shift_compat An n) ; ring. apply Rseq_cv_plus_compat ; [assumption | apply Rseq_constant_cv]. Qed.
imports: Rsequence Rseries_def