proposition: Lemma Rser_cv_sig_shifts_rev: forall k An, {l | Rser_cv (Rseq_shifts An k) l} -> {l | Rser_cv An l}.
proof: Proof. intros [| k] An [l Hl]. exists l ; eapply Rser_cv_ext ; [symmetry ; apply Rseq_shifts_0 | assumption]. exists (l + Rseq_sum An k) ; apply Rser_cv_shifts_rev ; assumption. Qed.
imports: Rsequence Rseries_def