coq-mathcomp-sum-of-two-square

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
homepage
https://github.com/thery/twoSquare
license
MIT
bugs tracker
https://github.com/thery/twoSquare/issues
dependencies
"ocaml" "coq" {>= "8.5"} "coq-mathcomp-ssreflect" {>= "1.6" & < "1.7"} "coq-mathcomp-algebra" {>= "1.6" & < "1.7"} "coq-mathcomp-field" {>= "1.6" & < "1.7"}
source
https://github.com/thery/twoSquare/archive/v1.0.0.zip
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-mathcomp-sum-of-two-square/coq-mathcomp-sum-of-two-square.1.0.0