case zero
m : ℕ
inst✝ : NeZero zero
⊢ succ 0 = 1

case succ
m n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
⊢ succ 0 = 1
n m : ℕ
inst✝ : NeZero n
⊢ succ 0 = 1
cases n
no goals
case zero
m : ℕ
inst✝ : NeZero zero
⊢ succ 0 = 1
exact (NeZero.ne 0 rfl).elim
no goals
case succ
m n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
⊢ succ 0 = 1
rfl