case mp =>
  intro (_ : Positive x)
  show ∃ (n : ℕ), Positive n ∧ x ≃ coe n
  have (Integer.NonzeroWithSign.intro
        (n : ℕ) (_ : Positive n) (_ : x ≃ 1 * coe n)) :=
    Impl.sign_props.positive_iff_sign_pos1.mp ‹Positive x›
  exists n
  apply And.intro ‹Positive n›
  show x ≃ coe n
  exact Rel.trans ‹x ≃ 1 * coe n› AA.identL
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
⊢ Positive x → ∃ n, Positive n ∧ x ≃ coe n
no goals