intro n h
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
⊢ ∀ {x_1 : ℕ}, f x_1 ≠ 0 → (↑x_1 ≤ x ↔ x_1 ∈ Iic ⌊x⌋₊)
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
n : ℕ
h : f n ≠ 0
⊢ ↑n ≤ x ↔ n ∈ Iic ⌊x⌋₊