proposition: Lemma is_ub_Rbar_dec (E : R -> Prop) : {l : R | is_ub_Rbar E l} + {(forall l : R, ~is_ub_Rbar E l)}.
proof: Proof. set (F (n : nat) (x : R) := x = 0 \/ (E x /\ x <= INR n)). assert (F_b : forall n, bound (F n)). intros ; exists (INR n) => x ; case => [-> | Hx]. by apply pos_INR. by apply Hx. assert (F_ex : forall n, (exists x : R, F n x)). intros ; exists 0 ; by left. set (u (n : nat) := proj1_sig (completeness (F n) (F_b n) (F_ex n))). destruct (LPO_ub_dec u) as [ [M HM] | HM]. + left ; exists M => x Hx. destruct (nfloor_ex (Rmax 0 x)) as [n Hn]. by apply Rmax_l. eapply Rle_trans, (HM (S n)). rewrite /u ; case: completeness => l Hl /=. apply Hl ; right ; split => //. rewrite S_INR ; eapply Rle_trans, Rlt_le, Hn. by apply Rmax_r. + right => l Hl. case: (HM (Rmax 0 l)) => n {HM}. apply Rle_not_lt. rewrite /u ; case: completeness => M HM /=. apply HM => x ; case => [ -> | Hx]. by apply Rmax_l. eapply Rle_trans, Rmax_r. apply Hl, Hx. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov