package coq-mathcomp-sum-of-two-square

gauss_int.v : the definition of gaussian integers

fermat2.v : the proof of Fermat's theorem

The final statement reads:

===================================================

From mathcomp Require Import all_ssreflect.

From mathcomp.contrib.sum_of_two_square Require Import gauss_int fermat2. Check sum2stest.

sum2stest : forall n : nat, reflect (forall p : nat, prime p -> odd p -> p %| n -> odd (logn p n) -> p %% 4 = 1) (n \is a sum_of_two_square)

===================================================