proposition: Lemma Rbar_lb_ub (E : Rbar -> Prop) (l : Rbar) : Rbar_is_lower_bound (fun x => E (Rbar_opp x)) (Rbar_opp l) <-> Rbar_is_upper_bound E l.
proof: Proof. split => Hl x Hx. apply Rbar_opp_le. apply Hl. by rewrite Rbar_opp_involutive. apply Rbar_opp_le. rewrite Rbar_opp_involutive. by apply Hl. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov