have hbz : b = 0 := add_left_eq_zero hab
case succ
b : Nat
hb : b ≠ zero
a' : Nat
ha : succ a' ≠ zero
hab : a' * b + b = zero
⊢ False
case succ
b : Nat
hb : b ≠ zero
a' : Nat
ha : succ a' ≠ zero
hab : a' * b + b = zero
hbz : b = 0
⊢ False