case step =>
  intro n (_ : step n * m ≃ 0)
  show step n ≃ 0 ∨ m ≃ 0
  apply Or.inr
  show m ≃ 0
  have : n * m + m ≃ 0 := calc
    n * m + m  ≃ _ := Rel.symm step_mul
    step n * m ≃ _ := ‹step n * m ≃ 0›
    0          ≃ _ := Rel.refl
  have ⟨_, (_ : m ≃ 0)⟩ := zero_sum_split ‹n * m + m ≃ 0›
  exact ‹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
no goals