intro (_ : sgn (n——m) ≃ s) (_ : sgn (k——j) ≃ s)
ℕ : Type
inst✝ : Natural ℕ
s : Difference ℕ
n m k j : ℕ
⊢ (n——m).sgn ≃ s → (k——j).sgn ≃ s → (n——m + k——j).sgn ≃ s
ℕ : Type
inst✝ : Natural ℕ
s : Difference ℕ
n m k j : ℕ
x✝¹ : (n——m).sgn ≃ s
x✝ : (k——j).sgn ≃ s
⊢ (n——m + k——j).sgn ≃ s