include "nat/permutation.ma".
include "nat/sigma_and_pi.ma".
include "nat/factorization.ma".
-include "nat/primes1.ma".
include "nat/times.ma".
include "nat/fermat_little_theorem.ma".
include "nat/nat.ma".
-include "legacy/coq.ma".
+(* FG: coq non c'entra con library, o sbaglio? *)
+(* include "legacy/coq.ma". *)
include "Z/compare.ma".
include "Z/plus.ma".
include "Z/times.ma".