proposition: Lemma lt_plus_epsilon_le: 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 + (x - y)). apply H. lra. Qed.
imports: Coq(Lra) ZornsLemma(EnsemblesImplicit ImageImplicit)