proposition: Lemma Rbar_glb_le_lub (E : Rbar -> Prop) : (exists x, E x) -> Rbar_le (Rbar_glb E) (Rbar_lub E).
proof: Proof. case => x Hex. apply Rbar_le_trans with x. unfold Rbar_glb ; case (Rbar_ex_glb _) ; simpl ; intros g (Hg, _) ; apply Hg ; auto. unfold Rbar_lub ; case (Rbar_ex_lub _) ; simpl ; intros l (Hl, _) ; apply Hl ; auto. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov