Formal target: Corpus.OEIS69922.conjecture

Question: for any $n > 0$, is there at least one prime $p$ such that $n^n \le p \le n^n + n^2$?

Exact formal statement

∀ (n : Nat), LT.lt.{0} 0 n → LE.le.{0} 1 (Corpus.OEIS69922.a n)

This target is a formal statement, not a proof of the problem.

Environment availability: available.