calc
  (n * p + m * q) + (k * q + j * p) ≃ _ := Rel.symm expand_swap
  (n + j) * p     + (k + m) * q     ≃ _ := AA.substL (AA.substL h)
  (k + m) * p     + (k + m) * q     ≃ _ := AA.substR (AA.substL (Rel.symm h))
  (k + m) * p     + (n + j) * q     ≃ _ := expand_swap
  (k * p + j * q) + (n * q + m * p) ≃ _ := Rel.refl
ℕ : Type
inst✝ : Natural ℕ
n m k j p q : ℕ
x✝ : n——m ≃ k——j
h : n + j ≃ k + m
⊢ n * p + m * q + (k * q + j * p) ≃ k * p + j * q + (n * q + m * p)
no goals