proposition: Lemma Rmetric_bound: forall x y z:R, R_metric x z < y - x -> z < y.
proof: Proof. intros. replace z with (x + (z-x)) by ring. apply Rle_lt_trans with (x + R_metric x z); [ assert (z - x <= R_metric x z) by apply Rle_abs | replace y with (x + (y-x)) by ring ]; lra. Qed.
imports: TopologicalSpaces OrderTopology MetricSpaces Coq(Lra Lia) ZornsLemma(EnsemblesTactics FiniteIntersections) RationalsInReals