proposition: Lemma Rbar_lb_p_infty (E : Rbar -> Prop) : Rbar_is_lower_bound E p_infty -> (forall x, E x -> x = p_infty).
proof: Proof. intros H x ; case x ; auto ; clear x ; [intros x| ] ; intros Hx. case (H _ Hx) ; simpl ; intuition. case (H _ Hx) ; simpl ; intuition. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov