case mpr =>
  intro (_ : sgn (n——m) ≃ -1)
  show Negative (n——m)
  have : ord_sgn (compare n m) ≃ (-1:Difference ℕ) := ‹sgn (n——m) ≃ -1›
  have : ord_sgn (compare n m) ≃ ord_sgn Ordering.lt := this
  have : compare n m = Ordering.lt := ord_sgn_inject this
  have : n < m := Natural.compare_lt.mp this
  have : Negative (n——m) := neg_diff_lt.mpr this
  exact this
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n——m).sgn ≃ -1 → Negative (n——m)
no goals