proposition: Lemma Rbar_ub_m_infty (E : Rbar -> Prop) : Rbar_is_upper_bound E m_infty -> forall x, E x -> x = m_infty.
proof: Proof. intros H [x| |] Hx ; now specialize (H _ Hx). Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov