∀[z:ℕ]. (isqrt(z * z) = z ∈ ℤ)
{ Auto }
1. z : ℕ
⊢ isqrt(z * z) = z ∈ ℤ