have (Nonzero.intro (sa : ℤ) (_ : Sqrt1 sa) nws) := ‹Nonzero a›
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
⊢ ∃ n, Positive n ∧ a * a ≃ coe (n * n)
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
sa : ℤ
sqrt1✝ : Sqrt1 sa
nws : NonzeroWithSign a sa
⊢ ∃ n, Positive n ∧ a * a ≃ coe (n * n)