n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑(val a) = (if val a ≤ n / 2 then ↑(val a) else ↑(val a) - ↑n) + ↑(if val a ≤ n / 2 then 0 else n)
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑(val a) = valMinAbs a + ↑(if val a ≤ n / 2 then 0 else n)
rw [valMinAbs_def_pos]
no goals
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑(val a) = (if val a ≤ n / 2 then ↑(val a) else ↑(val a) - ↑n) + ↑(if val a ≤ n / 2 then 0 else n)
split_ifs <;> simp [add_zero, sub_add_cancel]