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 n : ℕ
ih : n * (m + k) ≃ n * m + n * k
⊢ step n * (m + k) ≃ step n * m + step n * k
no goals