n m : ℕ
⊢ n * m + m = 0 → succ n = 0 ∨ m = 0
n m : ℕ
⊢ succ n * m = 0 → succ n = 0 ∨ m = 0
rw [succ_mul]
n m : ℕ
h : n * m + m = 0
⊢ succ n = 0 ∨ m = 0
n m : ℕ
⊢ n * m + m = 0 → succ n = 0 ∨ m = 0
intro h
no goals
n m : ℕ
h : n * m + m = 0
⊢ succ n = 0 ∨ m = 0
exact Or.inr (Nat.eq_zero_of_add_eq_zero_left h)