rw [succ_mul] at hab
case succ
b : Nat
hb : b ≠ zero
a' : Nat
ha : succ a' ≠ zero
hab : succ a' * b = zero
⊢ False
case succ
b : Nat
hb : b ≠ zero
a' : Nat
ha : succ a' ≠ zero
hab : a' * b + b = zero
⊢ False