have : sgn (n——m + k——j) ≃ s := calc
  sgn (n——m + k——j)                 ≃ _ := Rel.refl
  sgn ((n + k)——(m + j))            ≃ _ := Rel.refl
  ord_sgn (compare (n + k) (m + j)) ≃ _ := ord_sgn_subst this
  ord_sgn (compare k j)             ≃ _ := ‹ord_sgn (compare k j) ≃ s›
  s                                 ≃ _ := Rel.refl
ℕ : Type
inst✝ : Natural ℕ
s : Difference ℕ
n m k j : ℕ
x✝¹ : (n——m).sgn ≃ s
x✝ : (k——j).sgn ≃ s
this✝³ : ord_sgn (compare n m) ≃ s
this✝² : ord_sgn (compare k j) ≃ s
this✝¹ : ord_sgn (compare n m) ≃ ord_sgn (compare k j)
this✝ : compare n m = compare k j
this : compare (n + k) (m + j) = compare k j
⊢ (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
this✝⁴ : ord_sgn (compare n m) ≃ s
this✝³ : ord_sgn (compare k j) ≃ s
this✝² : ord_sgn (compare n m) ≃ ord_sgn (compare k j)
this✝¹ : compare n m = compare k j
this✝ : compare (n + k) (m + j) = compare k j
this : (n——m + k——j).sgn ≃ s
⊢ (n——m + k——j).sgn ≃ s