proposition: Lemma CV_shift_S : forall Un l, Un_cv Un l -> Un_cv (fun n => Un (S n)) l.
proof: Proof. intros Un l; unfold Un_cv; intros H_lim eps H_eps. destruct (H_lim eps H_eps) as [N H_N]. exists (S N). intros [|n] H_n. red in H_n; apply False_ind; apply (Nat.nle_succ_0 _ H_n). apply H_N; red; apply Nat.le_trans with n. apply le_S_n; trivial. repeat constructor. Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)