case mp =>
  intro (_ : Negative a)
  show Positive (-a)
  have : NonzeroWithSign a (-1) := negative_iff_sign_neg1.mp ‹Negative a›
  have : NonzeroWithSign (-a) 1 :=
    nonzeroWithSign_swap_neg.mpr ‹NonzeroWithSign a (-1)›
  have : Positive (-a) := positive_iff_sign_pos1.mpr ‹NonzeroWithSign (-a) 1›
  exact this
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Negative a → Positive (-a)
no goals