proposition: Lemma Rbar_opp_lub_glb (E : Rbar -> Prop) : Rbar_lub (fun x => E (Rbar_opp x)) = Rbar_opp (Rbar_glb 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 Hl', Rbar_lb_ub ; rewrite Rbar_opp_involutive ; apply (Rbar_is_lb_subset _ E) ; auto ; intros x ; rewrite Rbar_opp_involutive ; auto. apply Rbar_opp_le ; rewrite Rbar_opp_involutive ; apply Hg', Rbar_ub_lb ; rewrite Rbar_opp_involutive ; auto. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov