proposition: Lemma Sup_seq_minor_lt (u : nat -> Rbar) (M : R) : Rbar_lt M (Sup_seq u) <-> exists n, Rbar_lt M (u n).
proof: Proof. rewrite /Sup_seq ; case: ex_sup_seq => l Hl ; simpl proj1_sig ; split => H. case: l Hl H => [l | | ] Hl H. apply Rminus_lt_0 in H. case: (proj2 (Hl (mkposreal _ H))) ; simpl pos => {Hl} n Hl. exists n. replace M with (l - (l - M)) by ring. by apply Hl. apply (Hl M). by []. case: H => n Hn. apply Rbar_lt_le_trans with (u n). exact: Hn. by apply is_sup_seq_major. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy