case zero
inst✝ : NeZero Nat.zero
⊢ Injective val

case succ
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
⊢ Injective val
n : ℕ
inst✝ : NeZero n
⊢ Injective val
cases n
case succ
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
a b : ZMod (Nat.succ n✝)
h : val a = val b
⊢ a = b
case succ
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
⊢ Injective val
intro a b h
case succ
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
a b : ZMod (Nat.succ n✝)
h : val a = val b
⊢ a = b
case succ
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
a b : ZMod (Nat.succ n✝)
h : val a = val b
⊢ a = b
dsimp [ZMod]
case succ.h
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
a b : ZMod (Nat.succ n✝)
h : val a = val b
⊢ ↑a = ↑b
case succ
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
a b : ZMod (Nat.succ n✝)
h : val a = val b
⊢ a = b
ext
no goals
case succ.h
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
a b : ZMod (Nat.succ n✝)
h : val a = val b
⊢ ↑a = ↑b
exact h
no goals
case zero
inst✝ : NeZero Nat.zero
⊢ Injective val
cases NeZero.ne 0 rfl