case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
inst✝ : NeZero Nat.zero
a : ZMod Nat.zero
⊢ ↑a = ↑(val a)

case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
a : ZMod (Nat.succ n✝)
⊢ ↑a = ↑(val a)
n : ℕ
R : Type u_1
inst✝¹ : AddGroupWithOne R
inst✝ : NeZero n
a : ZMod n
⊢ ↑a = ↑(val a)
cases n
no goals
case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
a : ZMod (Nat.succ n✝)
⊢ ↑a = ↑(val a)
rfl
no goals
case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
inst✝ : NeZero Nat.zero
a : ZMod Nat.zero
⊢ ↑a = ↑(val a)
cases NeZero.ne 0 rfl