calc
  step n * step m        ≃ _ := step_mul
  n * step m + step m    ≃ _ := AA.substL ih
  (n * m + n) + step m   ≃ _ := add_step
  step ((n * m + n) + m) ≃ _ := AA.subst₁ AA.assoc
  step (n * m + (n + m)) ≃ _ := AA.subst₁ (AA.substR AA.comm)
  step (n * m + (m + n)) ≃ _ := AA.subst₁ (Rel.symm AA.assoc)
  step ((n * m + m) + n) ≃ _ := AA.subst₁ (AA.substL (Rel.symm step_mul))
  step (step n * m + n)  ≃ _ := Rel.symm add_step
  step n * m + step n    ≃ _ := Rel.refl
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
ih : n * step m ≃ n * m + n
⊢ step n * step m ≃ step n * m + step n
no goals