proposition: Lemma CV_shift' : forall f k l, Un_cv f l -> Un_cv (fun n => f (n + k)%nat) l.
proof: Proof. intros f' k l cvf eps ep; destruct (cvf eps ep) as [N Pn]. exists N; intros n nN; apply Pn; auto with arith. Qed.
imports: Rbase Rfunctions Compare