proposition: Lemma is_glb_Rbar_unique (E : R -> Prop) (l : Rbar) : is_glb_Rbar E l -> Glb_Rbar E = l.
proof: Proof. move => Hl ; rewrite /Glb_Rbar ; case: ex_glb_Rbar => l' /= Hl'. apply Rbar_le_antisym. by apply Hl, Hl'. by apply Hl', Hl. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov