case zero
inst✝ : NeZero Nat.zero
x : ZMod Nat.zero
⊢ valMinAbs x = if val x ≤ Nat.zero / 2 then ↑(val x) else ↑(val x) - ↑Nat.zero

case succ
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
x : ZMod (Nat.succ n✝)
⊢ valMinAbs x = if val x ≤ Nat.succ n✝ / 2 then ↑(val x) else ↑(val x) - ↑(Nat.succ n✝)
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ valMinAbs x = if val x ≤ n / 2 then ↑(val x) else ↑(val x) - ↑n
cases n
no goals
case zero
inst✝ : NeZero Nat.zero
x : ZMod Nat.zero
⊢ valMinAbs x = if val x ≤ Nat.zero / 2 then ↑(val x) else ↑(val x) - ↑Nat.zero
cases NeZero.ne 0 rfl
no goals
case succ
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
x : ZMod (Nat.succ n✝)
⊢ valMinAbs x = if val x ≤ Nat.succ n✝ / 2 then ↑(val x) else ↑(val x) - ↑(Nat.succ n✝)
rfl