calc
  m + k ≃ _ := AA.comm
  k + m ≃ _ := Rel.symm ‹n + j ≃ k + m›
  n + j ≃ _ := AA.comm
  j + n ≃ _ := Rel.refl
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ m + k ≃ j + n
no goals