case mp =>
  intro (_ : a < b)
  show sgn (a - b) ≃ -1
  have : Negative (a - b) := lt_iff_neg_diff.mp ‹a < b›
  have : sgn (a - b) ≃ -1 := sgn_negative.mp this
  exact this
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ a < b → sgn (a - b) ≃ -1
no goals