a✝ b : ℤ
n✝ : ℕ
a : ℤ
n : ℕ
⊢ a ≤ ↑n ∧ 0 ≤ ↑n ↔ a ≤ ↑n
a✝ b : ℤ
n✝ : ℕ
a : ℤ
n : ℕ
⊢ toNat a ≤ n ↔ a ≤ ↑n
rw [ofNat_le.symm, toNat_eq_max, max_le_iff]
no goals
a✝ b : ℤ
n✝ : ℕ
a : ℤ
n : ℕ
⊢ a ≤ ↑n ∧ 0 ≤ ↑n ↔ a ≤ ↑n
exact and_iff_left (ofNat_zero_le _)