proposition: Lemma Rbar_lb_dec (E : Rbar -> Prop) (Hm : ~ E m_infty) : {M : R | Rbar_is_lower_bound E (Finite M)} + {(forall M, ~Rbar_is_lower_bound E (Finite M))}.
proof: Proof. destruct (Rbar_ub_dec (fun x => E (Rbar_opp x)) Hm) as [(M, H)|H]. left ; exists (-M). apply Rbar_ub_lb ; simpl ; rewrite (Ropp_involutive M) ; auto. right ; intro M ; generalize (H (-M)) ; clear H ; intro H ; contradict H ; apply (Rbar_ub_lb E (Finite M)) ; auto. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov