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