have : n + j ≃ k + m := ‹n——m ≃ k——j›
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
x✝ : n——m ≃ k——j
⊢ -n——m ≃ -k——j
ℕ : Type
inst✝ : Natural ℕ
n m k j : ℕ
x✝ : n——m ≃ k——j
this : n + j ≃ k + m
⊢ -n——m ≃ -k——j