theorem Legendre.hasLegendrePrime_one : HasLegendrePrime 1

theorem Legendre.hasLegendrePrime_two : HasLegendrePrime 2

theorem Legendre.hasLegendrePrime_three : HasLegendrePrime 3

theorem Legendre.hasLegendrePrime_four : HasLegendrePrime 4

theorem Legendre.hasLegendrePrime_five : HasLegendrePrime 5

theorem Legendre.interval_width (n : ℕ) : (n + 1) ^ 2 - n ^ 2 = 2 * n + 1

TODO: Prove exact interval width (n + 1)^2 - n^2 = 2n + 1.

theorem Legendre.square_monotone {m n : ℕ} (hmn : m ≤ n) : m ^ 2 ≤ n ^ 2

TODO: Add reusable monotonicity lemmas for square endpoints.

theorem Legendre.lower_endpoint_nonprime {n : ℕ} (hn : 2 ≤ n) : ¬Nat.Prime (n ^ 2)

TODO: Show lower endpoint n^2 is composite for 2 ≤ n.