proposition: Lemma is_lub_Rbar_opp (E : R -> Prop) (l : Rbar) : is_glb_Rbar E l <-> is_lub_Rbar (fun x => E (- x)) (Rbar_opp l).
proof: Proof. split => [[lb glb] | [ub lub] ] ; split. by apply is_ub_Rbar_opp. intros b Hb. apply Rbar_opp_le ; rewrite Rbar_opp_involutive. apply glb, is_ub_Rbar_opp ; by rewrite Rbar_opp_involutive. by apply is_ub_Rbar_opp. intros b Hb. apply Rbar_opp_le. by apply lub, is_ub_Rbar_opp. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov