case mpr =>
  intro (_ : -b ≤ -a)
  show a ≤ b
  have : -b < -a ∨ -b ≃ -a := le_iff_lt_or_eqv.mp ‹-b ≤ -a›
  match this with
  | Or.inl (_ : -b < -a) =>
    have : a < b := lt_neg_flip.mpr ‹-b < -a›
    have : a ≤ b := le_iff_lt_or_eqv.mpr (Or.inl this)
    exact this
  | Or.inr (_ : -b ≃ -a) =>
    have : a ≃ b := AA.inject (Rel.symm ‹-b ≃ -a›)
    have : a ≤ b := le_iff_lt_or_eqv.mpr (Or.inr this)
    exact this
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ -b ≤ -a → a ≤ b
no goals