proposition: Lemma Rbar_ub_dec (E : Rbar -> Prop) (Hp : ~ E p_infty) : {M : R | Rbar_is_upper_bound E M} + {(forall (M : R), ~Rbar_is_upper_bound E M)}.
proof: Proof. destruct (is_ub_Rbar_dec E) as [ [M HM] | HM ]. left ; exists M ; case => [x | | ] //= Hx. by apply HM. right => M. specialize (HM M). contradict HM => x Hx. by apply HM. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov