proposition: Lemma Rser_cv_shift_rev2: forall Un l, Rser_cv (Rseq_shift Un) (l - (Un O)) -> Rser_cv Un l.
proof: Proof. intros ; replace l with (l - Un O + Un O) by ring ; apply Rser_cv_shift_rev ; assumption. Qed.
imports: Rsequence Rseries_def