theorem Oppermann.hasOppermannPrimes_two_to_five {n : ℕ} (hn2 : 2 ≤ n) (hn5 : n ≤ 5) : HasOppermannPrimes n

theorem Oppermann.hasOppermannPrimes_two_to_tenThousand {n : ℕ} (hn2 : 2 ≤ n) (hnB : n ≤ 10000) : HasOppermannPrimes n

TODO: Replace this with a computationally certified large finite range theorem.