proposition: Lemma glb_approx: forall (S:Ensemble R) (m:R) (eps:R), is_glb S m -> eps > 0 -> exists x:R, In S x /\ m <= x < m + eps.
proof: Proof. intros. assert (exists x:R, In S x /\ x < m + eps). { apply NNPP; intro. pose proof (not_ex_all_not _ _ H1). clear H1. simpl in H2. assert (is_lower_bound S (m+eps)). { red. intros. assert (~ x < m + eps). { intro. contradiction (H2 x). now split. } destruct (total_order_T x (m+eps)) as [[?|?]|?]; auto with real. - now contradiction H3. - destruct H. lra. } destruct H. pose proof (H3 _ H1). lra. } destruct H1 as [x [? ?]]. exists x. repeat split; trivial. destruct H. cut_by_lra (x >= m). auto with real. Qed.
imports: Coq(Lra) ZornsLemma(EnsemblesImplicit ImageImplicit)