proposition: Lemma Lim_seq_le_loc (u v : nat -> R) : eventually (fun n => u n <= v n) -> Rbar_le (Lim_seq u) (Lim_seq v).
proof: Proof. intros. move: (LimSup_le _ _ H) (LimInf_le _ _ H). move: (LimSup_LimInf_seq_le u) (LimSup_LimInf_seq_le v). unfold Lim_seq. case: (LimSup_seq u) => [lsu | | ] //= ; case: (LimInf_seq u) => [liu | | ] //= ; case: (LimSup_seq v) => [lsv | | ] //= ; case: (LimInf_seq v) => [liv | | ] //= ; intros. apply Rmult_le_compat_r. apply Rlt_le, Rinv_0_lt_compat, Rlt_0_2. by apply Rplus_le_compat. by apply Req_le. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy