theorem Oppermann.hasOppermannPrimes_two : HasOppermannPrimes 2

theorem Oppermann.hasOppermannPrimes_three : HasOppermannPrimes 3

theorem Oppermann.hasOppermannPrimes_four : HasOppermannPrimes 4

theorem Oppermann.hasOppermannPrimes_five : HasOppermannPrimes 5

theorem Oppermann.HasOppermannPrimes.lower_prime {n : ℕ} (h : HasOppermannPrimes n) : ∃ (p : ℕ), Nat.Prime p ∧ InLowerOppermannInterval n p

theorem Oppermann.HasOppermannPrimes.upper_prime {n : ℕ} (h : HasOppermannPrimes n) : ∃ (q : ℕ), Nat.Prime q ∧ InUpperOppermannInterval n q

theorem Oppermann.hasPrimeBetweenSquares_of_hasOppermannPrimes_succ {n : ℕ} (h : HasOppermannPrimes (n + 1)) : HasPrimeBetweenSquares n

Oppermann at n + 1 yields a Legendre-style prime between n^2 and (n + 1)^2.

theorem Oppermann.lower_interval_width (n : ℕ) : n ^ 2 - n * (n - 1) = n

TODO: Prove lower interval width is exactly n.

theorem Oppermann.upper_interval_width (n : ℕ) : n * (n + 1) - n ^ 2 = n

TODO: Prove upper interval width is exactly n.

theorem Oppermann.interval_separation_todo : True

TODO: Derive disjointness and ordering facts for the two Oppermann intervals.