n✝ m✝ : Nat
h✝ : n✝ * m✝ = 0
n m : Nat
h : n * m + m = 0
⊢ n + 1 = 0 ∨ m = 0
n✝ m✝ : Nat
h✝ : n✝ * m✝ = 0
n m : Nat
h : (n + 1) * m = 0
⊢ n + 1 = 0 ∨ m = 0
rw [succ_mul] at h
no goals
n✝ m✝ : Nat
h✝ : n✝ * m✝ = 0
n m : Nat
h : n * m + m = 0
⊢ n + 1 = 0 ∨ m = 0
exact .inr (Nat.eq_zero_of_add_eq_zero_left h)
no goals
n m : Nat
h : m = 0
⊢ n * m = 0
simp [h]