proposition: Lemma Rbar_ex_glb (E : Rbar -> Prop) : {l : Rbar | Rbar_is_glb E l}.
proof: Proof. destruct (Rbar_ex_lub (fun x => E (Rbar_opp x))) as [l Hl]. exists (Rbar_opp l). now apply Rbar_lub_glb ; rewrite Rbar_opp_involutive. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov