proposition: Lemma Rbar_ex_lub (E : Rbar -> Prop) : {l : Rbar | Rbar_is_lub E l}.
proof: Proof. destruct (EM_dec (E p_infty)) as [Hp|Hp]. exists p_infty ; split. by case. intros b Hb. apply Rbar_not_lt_le. contradict Hp => H. apply: Rbar_le_not_lt Hp. by apply Hb. destruct (ex_lub_Rbar E) as [l Hl]. exists l ; split. case => [x | | ] // Hx. by apply Hl. intros b Hb. apply Hl => x Hx. by apply Hb. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov