Wilson's theorem. #
This file contains a proof of Wilson's theorem.
The heavy lifting is mostly done by the previous
but here we also prove the other logical direction.
This could be generalized to similar results about finite abelian groups.
wilsons_lemmainto this file, and give it a descriptive name.