proposition: Lemma is_LimSup_seq_ind_k (u : nat -> R) (k : nat) (l : Rbar) : is_LimSup_seq u l <-> is_LimSup_seq (fun n => u (n + k)%nat) l.
proof: Proof. elim: k u => [ | k IH] /= u. split ; apply is_LimSup_seq_ext => n ; by rewrite -plus_n_O. rewrite is_LimSup_seq_ind_1. rewrite (IH (fun n => u (S n))). split ; apply is_LimSup_seq_ext => n ; by rewrite plus_n_Sm. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy