cases eq_zero_or_eq_zero_of_mul_eq_zero h with
| inl ha => contradiction
| inr hb => assumption
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ : Nat
h : a * succ b' = zero
⊢ succ b' = zero
no goals