apply Iff.intro
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
⊢ Positive x ↔ ∃ n, Positive n ∧ x ≃ coe n
case mp
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
⊢ Positive x → ∃ n, Positive n ∧ x ≃ coe n

case mpr
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
⊢ (∃ n, Positive n ∧ x ≃ coe n) → Positive x