case zero
x : ZMod Nat.zero
⊢ valMinAbs x = 0 ↔ x = 0

case succ
n : ℕ
x : ZMod (Nat.succ n)
⊢ valMinAbs x = 0 ↔ x = 0
n : ℕ
x : ZMod n
⊢ valMinAbs x = 0 ↔ x = 0
cases' n with n
case succ
n : ℕ
x : ZMod (Nat.succ n)
⊢ valMinAbs x = valMinAbs 0 ↔ x = 0
case succ
n : ℕ
x : ZMod (Nat.succ n)
⊢ valMinAbs x = 0 ↔ x = 0
rw [← valMinAbs_zero n.succ]
no goals
case succ
n : ℕ
x : ZMod (Nat.succ n)
⊢ valMinAbs x = valMinAbs 0 ↔ x = 0
apply injective_valMinAbs.eq_iff
no goals
case zero
x : ZMod Nat.zero
⊢ valMinAbs x = 0 ↔ x = 0
simp