exists n
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
x✝ : Positive x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ 1 * coe n
⊢ ∃ n, Positive n ∧ x ≃ coe n
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
x✝ : Positive x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ 1 * coe n
⊢ Positive n ∧ x ≃ coe n