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