case zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : NeZero Nat.zero
⊢ Nat.cast ∘ val = cast

case succ
R : Type u_1
inst✝¹ : Ring R
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
⊢ Nat.cast ∘ val = cast
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : NeZero n
⊢ Nat.cast ∘ val = cast
cases n
no goals
case succ
R : Type u_1
inst✝¹ : Ring R
n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
⊢ Nat.cast ∘ val = cast
rfl
no goals
case zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : NeZero Nat.zero
⊢ Nat.cast ∘ val = cast
cases NeZero.ne 0 rfl