intro h
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ : Nat
⊢ a * succ b' = a * zero → succ b' = zero
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ : Nat
h : a * succ b' = a * zero
⊢ succ b' = zero