Legendre's conjecture

Reference: Wikipedia

theorem legendre_conjecture : (∀ n ≥ 1, ∃ p ∈ Set.Ioo (n ^ 2) ((n + 1) ^ 2), Prime p) ↔ sorry

Does there always exist at least one prime between consecutive perfect squares?