For every integer $x \ge 2$ there exists a prime between $x(x-1)$ and $x^2$.

Exact retained declaration excerpt — not the whole file.

/--
For every integer $x \ge 2$ there exists a prime between $x(x-1)$ and $x^2$.
-/
@[category research open, AMS 11]
theorem oppermann_conjecture.parts.i (x : ℕ) (hx : 2 ≤ x) :
    ∃ p ∈ Ioo (x * (x - 1)) (x^2), p.Prime := by
  sorry