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