proposition: Lemma Rbar_lub_glb (E : Rbar -> Prop) (l : Rbar) : Rbar_is_lub (fun x => E (Rbar_opp x)) (Rbar_opp l) <-> Rbar_is_glb E l.
proof: Proof. split ; [intros (ub, lub) | intros (lb, glb)] ; split. apply Rbar_ub_lb ; auto. intros b Hb ; generalize (lub _ (proj2 (Rbar_ub_lb _ _) Hb)) ; apply Rbar_opp_le. apply Rbar_lb_ub ; intros x ; simpl ; repeat rewrite Rbar_opp_involutive ; apply lb. intros b Hb. apply Rbar_opp_le ; rewrite Rbar_opp_involutive ; apply glb, Rbar_ub_lb ; rewrite Rbar_opp_involutive ; auto. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov