Solution (source code)

= Solution

The <modular congruence> $x^4\equiv1$ first implies $x\not\equiv0$. Multiplication by such an $x$ permutes the nonzero <residue classes> modulo the prime $p$: if $xa\equiv xb$, cancellation gives $a\equiv b$. Multiply all these residues and cancel their nonzero product to obtain $x^{p-1}\equiv1$, the usual short proof of <Fermat little theorem>.

Now $(x^2-1)(x^2+1)\equiv0$. By the <Euclid lemma>, either $x^2\equiv1$ or $x^2\equiv-1$. In the latter case, because $p-1=4k+2$,
$$
x^{p-1}=(x^2)^{2k+1}\equiv(-1)^{2k+1}=-1\pmod p,
$$
contradicting the preceding product argument, since $p$ is odd. Thus
$$
\boxed{x^2\equiv1\pmod p}.
$$
No unproved assertion about the number of fourth roots is needed.