proposition: Lemma is_sup_seq_major (u : nat -> Rbar) (l : Rbar) (n : nat) : is_sup_seq u l -> Rbar_le (u n) l.
proof: Proof. case: l => [l | | ] //= Hl. move: (fun eps => proj1 (Hl eps) n) => {Hl}. case: (u n) => [un | | ] //= Hun. apply le_epsilon => e He ; apply Rlt_le. apply: Hun (mkposreal e He). by move: (Hun (mkposreal _ Rlt_0_1)). case: (u n) => [un | | ] //. move: (Hl (u n) n) ; case: (u n) => [un | | ] //= {} Hl. by apply Rlt_irrefl in Hl. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy