case mp =>
  intro (_ : a ≤ b)
  show -b ≤ -a
  have : a < b ∨ a ≃ b := le_iff_lt_or_eqv.mp ‹a ≤ b›
  match this with
  | Or.inl (_ : a < b) =>
    have : -b < -a := lt_neg_flip.mp ‹a < b›
    have : -b ≤ -a := le_iff_lt_or_eqv.mpr (Or.inl this)
    exact this
  | Or.inr (_ : a ≃ b) =>
    have : -b ≃ -a := AA.subst₁ (Rel.symm ‹a ≃ b›)
    have : -b ≤ -a := 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 : ℤ
⊢ a ≤ b → -b ≤ -a
no goals