proposition: Lemma Glb_Rbar_eqset (E1 E2 : R -> Prop) : (forall x, E1 x <-> E2 x) -> Glb_Rbar E1 = Glb_Rbar E2.
proof: Proof. move => H ; rewrite {2}/Glb_Rbar ; case: (ex_glb_Rbar E2) => l2 H2 /=. apply is_glb_Rbar_unique. move: H2 ; by apply is_glb_Rbar_eqset. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov