case zero
n : ℕ
R : Type ?u.21503
inst✝ : NeZero Nat.zero
a : ZMod Nat.zero
⊢ ↑(val a) = a

case succ
n : ℕ
R : Type ?u.21503
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
a : ZMod (Nat.succ n✝)
⊢ ↑(val a) = a
n✝ : ℕ
R : Type ?u.21503
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑(val a) = a
cases n
no goals
case zero
n : ℕ
R : Type ?u.21503
inst✝ : NeZero Nat.zero
a : ZMod Nat.zero
⊢ ↑(val a) = a
cases NeZero.ne 0 rfl
no goals
case succ
n : ℕ
R : Type ?u.21503
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
a : ZMod (Nat.succ n✝)
⊢ ↑(val a) = a
apply Fin.cast_val_eq_self