have hn : n' = succ n' := by exact succ_inj h
case succ
n' : Nat
ih : n' ≠ succ n'
h : succ n' = succ (succ n')
⊢ False
case succ
n' : Nat
ih : n' ≠ succ n'
h : succ n' = succ (succ n')
hn : n' = succ n'
⊢ False