feat(number_theory/wilson): add Wilson's Theorem (#14717)
The previous "Wilson's lemma" (zmod.wilsons_lemma) was a single direction of the iff for Wilson's Theorem. This finishes the proof by adding the (admittedly, much simpler) direction where, if the congruence is satisfied for `n`, then `n` is prime.
