proposition: Lemma ex_glb_Rbar (E : R -> Prop) : {l : Rbar | is_glb_Rbar E l}.
proof: Proof. case: (ex_lub_Rbar (fun x => E (- x))) => l Hl. exists (Rbar_opp l). apply is_lub_Rbar_opp ; by rewrite Rbar_opp_involutive. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov