proposition: Lemma Rbar_lb_le_ub (E : Rbar -> Prop) (l1 l2 : Rbar) : (exists x, E x) -> Rbar_is_lower_bound E l1 -> Rbar_is_upper_bound E l2 -> Rbar_le l1 l2.
proof: Proof. intros (x, Hex) Hl Hu ; apply Rbar_le_trans with (y := x) ; [apply Hl | apply Hu] ; auto. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov