github.com/coq/opam-coq-archive
The formal proof of the Feit-Thompson theorem
opam install coq-mathcomp-odd-order.1.6.2