proposition: Lemma ex_sup_seq (u : nat -> Rbar) : {l : Rbar | is_sup_seq u l}.
proof: Proof. case (LPO (fun n => p_infty = u n)) => [/= | [np Hnp] | Hnp]. intro n0 ; destruct (u n0) as [r | | ]. now right. left ; auto. now right. exists p_infty => M. exists np ; by rewrite -Hnp. case (Rbar_ex_lub (fun x => exists n, x = u n)). intros l Hl ; exists l ; apply Rbar_is_lub_sup_seq ; auto. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy