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