proposition: Lemma gt_minus_epsilon_ge: forall x y:R, (forall eps:R, eps > 0 -> x > y - eps) -> x >= y.
proof: Proof. intros. destruct (total_order_T x y) as [[?|?]|?]; lra || cut_by_lra (x > y - (y - x)). apply H. lra. Qed.
imports: Coq(Lra) ZornsLemma(EnsemblesImplicit ImageImplicit)