proposition: Lemma Rbar_opp_glb_lub (E : Rbar -> Prop) : Rbar_glb (fun x => E (Rbar_opp x)) = Rbar_opp (Rbar_lub E).
proof: Proof. unfold Rbar_glb ; case (Rbar_ex_glb _) ; simpl ; intros g [Hg Hg'] ; unfold Rbar_lub ; case (Rbar_ex_lub _) ; simpl ; intros l [Hl Hl'] ; apply Rbar_le_antisym. apply Rbar_opp_le ; rewrite Rbar_opp_involutive ; apply Hl', Rbar_lb_ub ; rewrite Rbar_opp_involutive ; auto. apply Hg', Rbar_lb_ub ; auto. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov