intro n (_ : step n * m ≃ 0)
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), step m_1 * m ≃ 0 → step m_1 ≃ 0 ∨ m ≃ 0
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
x✝ : step n * m ≃ 0
⊢ step n ≃ 0 ∨ m ≃ 0