Is it true that, for every prime $p$, there is a prime $q \leq p$ which is a primitive root modulo $p$?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

1sorry ↔ ∀ (p : ℕ), Nat.Prime p → p ≠ 2 → ∃ q, Nat.Prime q ∧ q < p ∧ orderOf ↑q = p - 1