proposition: Lemma is_lb_Rbar_opp (E : R -> Prop) (l : Rbar) : is_ub_Rbar E l <-> is_lb_Rbar (fun x => E (- x)) (Rbar_opp l).
proof: Proof. split ; intros Hl x Hx ; apply Rbar_opp_le. now rewrite Rbar_opp_involutive ; apply Hl. now apply Hl ; rewrite Ropp_involutive. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov