case succ b' IH' => {
 intros A B;
 simp [Nat.mul];
}
a' : ℕ
IH : ∀ (b : ℕ), a' ≠ 0 → b ≠ 0 → a' * b ≠ 0
b' : ℕ
IH' : succ a' ≠ 0 → b' ≠ 0 → succ a' * b' ≠ 0
⊢ succ a' ≠ 0 → succ b' ≠ 0 → succ a' * succ b' ≠ 0
no goals