have _ : succ a' * succ b' ≠ zero := by
  apply mul_pos <;> assumption
a b a' b' : Nat
x✝ : succ a' * succ b' = zero
ha' : succ a' ≠ zero
hb' : succ b' ≠ zero
⊢ succ a' = 0 ∨ succ b' = 0
a b a' b' : Nat
x✝¹ : succ a' * succ b' = zero
ha' : succ a' ≠ zero
hb' : succ b' ≠ zero
x✝ : succ a' * succ b' ≠ zero
⊢ succ a' = 0 ∨ succ b' = 0