Legendre's conjecture

References:

• Landau Problems Wikipedia Page
• Legendre Conjecture Wikipedia Page

theorem LegendreConjecture.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?