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