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