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