Solution (source code)

= Solution

<Lagrange theorem for polynomial congruences> says that a nonzero <polynomial> of degree $d$ over a <field> has at most $d$ distinct <roots of a polynomial>. It follows by repeatedly factoring out $x-a$ at a root. Over the <finite field> $\mathbb F_p$, the only solutions of $x^2=1$ are $1$ and $-1$: these are distinct because $p$ is odd, and the root bound excludes any others.

Every nonzero element has a unique <multiplicative inverse>. Pair each element of $\mathbb F_p^\times$ with its inverse. All pairs of distinct elements contribute $1$ to the product; the only unpaired elements are $1$ and $-1$. Thus <Wilson theorem> follows:
$$
\boxed{(p-1)!\equiv-1\pmod p.}
$$
If Lagrange's theorem is formulated for <finite groups>, it states that the order of a <subgroup> divides the order of the group; in particular every element of $\mathbb F_p^\times$ has order dividing $p-1$. The inverse-pairing proof above establishes the required congruence directly.