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