show m + k ≃ j + n
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ m——n ≃ j——k
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ m + k ≃ j + n