proposition: Lemma is_lim_seq_incr_1 (u : nat -> R) (l : Rbar) : is_lim_seq u l <-> is_lim_seq (fun n => u (S n)) l.
proof: Proof. split ; intros H P HP ; destruct (H P HP) as [N HN]. - exists N. intros n Hn. apply HN. now apply le_S. - exists (S N). intros n Hn. destruct n as [|n] ; try easy. apply HN. now apply le_S_n. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy