have : n < m := neg_diff_lt.mp ‹Negative (n——m)›
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Negative (n——m)
⊢ (n——m).sgn ≃ -1
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Negative (n——m)
this : n < m
⊢ (n——m).sgn ≃ -1