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

Exact retained declaration excerpt — not the whole file.

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