proposition: Lemma Lim_seq_incr_n (u : nat -> R) (N : nat) : Lim_seq (fun n => u (n + N)%nat) = Lim_seq u.
proof: Proof. elim: N u => [ | N IH] u. apply Lim_seq_ext => n ; by rewrite Nat.add_0_r. rewrite -(Lim_seq_incr_1 u) -(IH (fun n => u (S n))). apply Lim_seq_ext => n ; by rewrite plus_n_Sm. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy