have : ord_sgn (compare n m) ≃ (-1:Difference ℕ) := this
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Negative (n——m)
this✝¹ : n < m
this✝ : compare n m = Ordering.lt
this : ord_sgn (compare n m) ≃ ord_sgn Ordering.lt
⊢ (n——m).sgn ≃ -1
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Negative (n——m)
this✝² : n < m
this✝¹ : compare n m = Ordering.lt
this✝ : ord_sgn (compare n m) ≃ ord_sgn Ordering.lt
this : ord_sgn (compare n m) ≃ -1
⊢ (n——m).sgn ≃ -1