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