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