proposition: Lemma is_LimSup_LimInf_seq_le (u : nat -> R) (ls li : Rbar) : is_LimSup_seq u ls -> is_LimInf_seq u li -> Rbar_le li ls.
proof: Proof. case: ls => [ls | | ] ; case: li => [li | | ] //= Hls Hli. apply le_epsilon => e He ; set eps := pos_div_2 (mkposreal e He). replace li with ((li - eps) + eps) by ring. replace (ls + e) with ((ls + eps) + eps) by (simpl ; field). apply Rplus_le_compat_r, Rlt_le. case: (proj2 (Hls eps)) => {Hls} Ns Hls. case: (proj2 (Hli eps)) => {Hli} Ni Hli. apply Rlt_trans with (u (Ns + Ni)%nat). apply Hli ; by intuition. apply Hls ; by intuition. case: (proj2 (Hls (mkposreal _ Rlt_0_1))) => {Hls} /= Ns Hls. case: (Hli (ls + 1)) => {Hli} Ni Hli. absurd (ls + 1 < u (Ns + Ni)%nat). apply Rle_not_lt, Rlt_le, Hls ; by intuition. apply Hli ; by intuition. case: (proj2 (Hli (mkposreal _ Rlt_0_1))) => {Hli} /= Ni Hli. case: (Hls (li - 1)) => {Hls} Ns Hls. absurd (li - 1 < u (Ns + Ni)%nat). apply Rle_not_lt, Rlt_le, Hls ; by intuition. apply Hli ; by intuition. case: (Hli 0) => {Hli} /= Ni Hli. case: (Hls 0) => {Hls} Ns Hls. absurd (0 < u (Ns + Ni)%nat). apply Rle_not_lt, Rlt_le, Hls ; by intuition. apply Hli ; by intuition. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy