intro (Exists.intro (n : ℕ) (And.intro (_ : Positive n) (_ : x ≃ coe n)))
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
⊢ (∃ n, Positive n ∧ x ≃ coe n) → Positive x
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
n : ℕ
left✝ : Positive n
right✝ : x ≃ coe n
⊢ Positive x