proposition: Lemma is_lb_Rbar_dec (E : R -> Prop) : {l : R | is_lb_Rbar E l} + {(forall l : R, ~is_lb_Rbar E l)}.
proof: Proof. destruct (is_ub_Rbar_dec (fun x => E (- x))) as [ [l Hl] | Hl ]. left ; exists (Rbar_opp l). by apply is_ub_Rbar_opp ; rewrite (Rbar_opp_involutive l). right => l. specialize (Hl (Rbar_opp l)). contradict Hl. by apply (is_ub_Rbar_opp E l). Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov