case mpr =>
  intro
    (Exists.intro (n : ℕ) (And.intro (_ : Positive n) (_ : x ≃ -(coe n))))
  show Negative x
  apply Impl.sign_props.negative_iff_sign_neg1.mpr
  show Integer.NonzeroWithSign x (-1)
  apply Integer.NonzeroWithSign.intro n ‹Positive n›
  show x ≃ -1 * coe n
  exact Rel.trans ‹x ≃ -(coe n)› (Rel.symm Integer.mul_neg_one)
x : ℤ
⊢ (∃ n, Positive n ∧ x ≃ -coe n) → Negative x
no goals