Solution
= Solution
Set $m=(p-1)/2$. Pairing each of $1,\ldots,m$ with its negative residue gives
$$
(p-1)!\equiv\prod_{j=1}^{m}j(p-j)
\equiv(-1)^m(m!)^2\pmod p.
$$
Here $p\equiv1\pmod4$ makes $m$ even. By <Wilson theorem>,
$$
\boxed{x=m!=\left(\frac{p-1}{2}\right)!\pmod p}
$$
satisfies $x^2\equiv-1\pmod p$. Its negative is the other root. This proves existence by an explicit <factorial> construction.