proposition: Lemma LimSup_le (u v : nat -> R) : eventually (fun n => u n <= v n) -> Rbar_le (LimSup_seq u) (LimSup_seq v).
proof: Proof. intros (N,H). rewrite /LimSup_seq. case: ex_LimSup_seq ; case => [lu | | ] //= Hlu ; case: ex_LimSup_seq ; case => [lv | | ] //= Hlv. apply Rnot_lt_le => Hl. apply Rminus_lt_0 in Hl. case: (Hlv (pos_div_2 (mkposreal _ Hl))) => {Hlv} /= _ [n Hlv]. case: (proj1 (Hlu (pos_div_2 (mkposreal _ Hl))) (N + n)%nat) => {Hlu} m /= [Hm Hlu]. move: (H _ (Nat.le_trans _ _ _ (Nat.le_add_r _ _) Hm)). apply Rlt_not_le. eapply Rlt_trans, Hlu. eapply Rlt_le_trans. eapply Hlv, Nat.le_trans, Hm. by apply MyNat.le_add_l. apply Req_le ; field. case: (Hlv (lu - 1)) => {Hlv} n Hlv. case: (proj1 (Hlu (mkposreal _ Rlt_0_1)) (N + n)%nat) => {Hlu} m /= [Hm Hlu]. move: (H _ (Nat.le_trans _ _ _ (Nat.le_add_r _ _) Hm)). apply Rlt_not_le. eapply Rlt_trans, Hlu. eapply Hlv, Nat.le_trans, Hm. by apply MyNat.le_add_l. case: (Hlv (mkposreal _ Rlt_0_1)) => {Hlv} /= _ [n Hlv]. case: (Hlu (lv + 1) (N + n)%nat) => {Hlu} /= m [Hm Hlu]. move: (H _ (Nat.le_trans _ _ _ (Nat.le_add_r _ _) Hm)). apply Rlt_not_le. eapply Rlt_trans, Hlu. eapply Hlv, Nat.le_trans, Hm. by apply MyNat.le_add_l. case: (Hlv 0) => {Hlv} n Hlv. case: (Hlu 0 (N + n)%nat) => {Hlu} m [Hm Hlu]. move: (H _ (Nat.le_trans _ _ _ (Nat.le_add_r _ _) Hm)). apply Rlt_not_le. eapply Rlt_trans, Hlu. eapply Hlv, Nat.le_trans, Hm. by apply MyNat.le_add_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy