proposition: Lemma is_LimInf_seq_ind_k (u : nat -> R) (k : nat) (l : Rbar) : is_LimInf_seq u l <-> is_LimInf_seq (fun n => u (n + k)%nat) l.
proof: Proof. rewrite -?is_LimSup_opp_LimInf_seq. by apply (is_LimSup_seq_ind_k (fun n => - u n)). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy