]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/library/nat/primes1.ma
.ma inclusions corrected/minimized
[helm.git] / helm / matita / library / nat / primes1.ma
index 55d643262e15b4d4201359a0a6f0c01d515c9871..3df3922a4887d50e19fc4ec3e0f5acfffadb2ec4 100644 (file)
@@ -16,7 +16,6 @@ set "baseuri" "cic:/matita/nat/primes1".
 
 include "datatypes/constructors.ma".
 include "nat/primes.ma".
-include "nat/exp.ma".
 
 (* p is just an upper bound, acc is an accumulator *)
 let rec n_divides_aux p n m acc \def