calc
  (n * k + m * j, n * j + m * k) ≃ _ := AA.substL (AA.substL AA.comm)
  (k * n + m * j, n * j + m * k) ≃ _ := AA.substL (AA.substR AA.comm)
  (k * n + j * m, n * j + m * k) ≃ _ := AA.substR (AA.substL AA.comm)
  (k * n + j * m, j * n + m * k) ≃ _ := AA.substR (AA.substR AA.comm)
  (k * n + j * m, j * n + k * m) ≃ _ := AA.substR AA.comm
  (k * n + j * m, k * m + j * n) ≃ _ := Rel.refl
case a
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
⊢ (n * k + m * j, n * j + m * k) ≃ (k * n + j * m, k * m + j * n)
no goals