proposition: Lemma LimInf_le (u v : nat -> R) : eventually (fun n => u n <= v n) -> Rbar_le (LimInf_seq u) (LimInf_seq v).
proof: Proof. intros. apply Rbar_opp_le. rewrite -!LimSup_seq_opp. apply LimSup_le. move: H ; apply filter_imp => n. by apply Ropp_le_contravar. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy