theorem Legendre.legendre_conjecture (n : ℕ) : 1 ≤ n → HasLegendrePrime n

Legendre's conjecture: for every n >= 1, there is a prime between n^2 and (n + 1)^2.

theorem Legendre.legendre_conjecture_between_squares (n : ℕ) : 1 ≤ n → ∃ (p : ℕ), Nat.Prime p ∧ n ^ 2 < p ∧ p < (n + 1) ^ 2

Expanded form of legendre_conjecture.

theorem Legendre.infinite_primes_from_legendre (hLeg : ∀ (n : ℕ), 1 ≤ n → HasLegendrePrime n) : {p : ℕ | Nat.Prime p}.Infinite

TODO: Derive infinitude of primes from a proof of Legendre.

theorem Legendre.prime_counting_lower_bound_from_legendre : True

TODO: Prove quantitative prime-counting lower bounds implied by Legendre.