intros b
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
⊢ ∀ (b : ℕ), succ a' ≠ 0 → b ≠ 0 → succ a' * b ≠ 0
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
b : ℕ
⊢ succ a' ≠ 0 → b ≠ 0 → succ a' * b ≠ 0