proposition: Lemma is_glb_Rbar_correct (E : R -> Prop) (l : Rbar) : is_glb_Rbar E l <-> Rbar_is_glb (fun x => is_finite x /\ E x) l.
proof: Proof. split => [[Hub Hlub]|[Hub Hlub]]. split ; [ | move => b Hb ; apply Hlub ] ; by apply is_lb_Rbar_correct. split ; [ | move => b Hb ; apply Hlub ] ; by apply is_lb_Rbar_correct. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov