n a : ℕ
inst✝ : NeZero n
ha : valMinAbs ↑a = ↑a
⊢ a ≤ n / 2
n a : ℕ
inst✝ : NeZero n
⊢ valMinAbs ↑a = ↑a ↔ a ≤ n / 2
refine' ⟨fun ha => _, valMinAbs_natCast_of_le_half⟩
n a : ℕ
inst✝ : NeZero n
ha : valMinAbs ↑a = ↑a
⊢ Int.natAbs (valMinAbs ↑a) ≤ n / 2
n a : ℕ
inst✝ : NeZero n
ha : valMinAbs ↑a = ↑a
⊢ a ≤ n / 2
rw [← Int.natAbs_ofNat a, ← ha]
no goals
n a : ℕ
inst✝ : NeZero n
ha : valMinAbs ↑a = ↑a
⊢ Int.natAbs (valMinAbs ↑a) ≤ n / 2
exact natAbs_valMinAbs_le a