proposition: Lemma Rser_cv_shifts_rev : forall k An l, Rser_cv (Rseq_shifts An (S k)) l -> Rser_cv An (l + Rseq_sum An k).
proof: Proof. intros k An l Hl ; apply Rseq_cv_shifts_compat with (S k) ; apply Rseq_cv_eq_compat with (Rseq_plus (Rseq_sum (Rseq_shifts An (S k))) (Rseq_sum An k)). intro n ; unfold Rseq_plus, Rseq_constant ; rewrite (Rseq_sum_shifts_compat An k n) ; ring. apply Rseq_cv_plus_compat ; [assumption | apply Rseq_constant_cv]. Qed.
imports: Rsequence Rseries_def