proposition: Lemma CR_cv_shift' : forall {R : ConstructiveReals} f k l, CR_cv R f l -> CR_cv R (fun n => f (n + k)%nat) l.
proof: Proof. intros R f' k l cvf eps; destruct (cvf eps) as [N Pn]. exists N; intros n nN; apply Pn; auto. apply Nat.le_trans with n; [ assumption | apply Nat.le_add_r ]. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs