apply Generic.negative_iff_sign_neg1.mpr
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
⊢ Negative (n——m)
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
⊢ NonzeroWithSign (n——m) (-1)