no goals
α : Type u
β : Type v
X : Type ?u.52437
ι : Type ?u.52440
inst✝ : PseudoMetricSpace α
x y z : α
δ ε✝ ε₁ ε₂ : ℝ
s : Set α
ε : ℝ
ε0 : 0 < ε
n : ℕ
hn : 1 / (↑n + 1) < ε
⊢ 1 / ↑(n + 1) ≤ ε
exact_mod_cast hn.le