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