proposition: Lemma Rbar_is_glb_unique (E : Rbar -> Prop) (l : Rbar) : Rbar_is_glb E l -> Rbar_glb E = l.
proof: Proof. move => H. rewrite /Rbar_glb. case: Rbar_ex_glb => l0 H0 /=. apply Rbar_le_antisym. apply H, H0. apply H0, H. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov