case step =>
  intro n (ih : n * m ≃ m * n)
  show step n * m ≃ m * step n
  calc
    step n * m ≃ _ := step_mul
    n * m + m  ≃ _ := AA.substL ih
    m * n + m  ≃ _ := Rel.symm mul_step
    m * step n ≃ _ := Rel.refl
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), m_1 * m ≃ m * m_1 → step m_1 * m ≃ m * step m_1
no goals