case mpr =>
  intro (_ : Negative (a - b))
  show a < b
  have : Negative (-(b - a)) :=
    AA.substFn (Rel.symm sub_neg_flip) ‹Negative (a - b)›
  have : Positive (b - a) :=
    positive_iff_negated_negative.mpr ‹Negative (-(b - a))›
  have : a < b := gt_iff_pos_diff.mpr ‹Positive (b - a)›
  exact this
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ Negative (a - b) → a < b
no goals