proposition: Lemma Rbar_lb_eq_ub (E : Rbar -> Prop) (l : Rbar) : Rbar_is_lower_bound E l -> Rbar_is_upper_bound E l -> forall x, E x -> x = l.
proof: Proof. intros Hl Hu x Hx. apply Rbar_le_antisym ; [apply Hu | apply Hl] ; auto. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov