proposition: Lemma Rser_cv_sig_shift_rev: forall An, {l | Rser_cv (Rseq_shift An) l} -> {l | Rser_cv An l}.
proof: Proof. intros An [l Hl] ; exists (l + An O) ; apply Rser_cv_shift_rev ; assumption. Qed.
imports: Rsequence Rseries_def