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