cases a with
| zero => exact ha (Eq.refl zero)  | succ a' =>
  rw [succ_mul] at hab
  have hbz : b = 0 := add_left_eq_zero hab
  exact hb hbz
a b : Nat
ha : a ≠ zero
hb : b ≠ zero
hab : a * b = zero
⊢ False
no goals