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