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