github.com/coq/opam-coq-archive
A proof of Fermat's theorem on sum of two squares. It is the proof that uses gaussian integers. This is done in ssreflect. It contains two file :
opam install coq-mathcomp-sum-of-two-square.1.0.0