The square test of Int.sqrt through the natural numbers

A candidate for Mathlib.Data.Int.Sqrt: Int.sqrt v squares to v exactly when v ≥ 0 and the square root of the natural number v.toNat squares to it (Int.sqrt_mul_self_eq_iff), the test that a program on natural numbers makes; Int.exists_mul_self turns the left side into ∃ n, n * n = v.

Main statements

• Int.sqrt_mul_self_eq_iff: sqrt v * sqrt v = v exactly when 0 ≤ v and v.toNat.sqrt * v.toNat.sqrt = v.toNat.

theorem Int.sqrt_mul_self_eq_iff (v : ℤ) : sqrt v * sqrt v = v ↔ 0 ≤ v ∧ v.toNat.sqrt * v.toNat.sqrt = v.toNat