X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fprimes1.ma;h=3df3922a4887d50e19fc4ec3e0f5acfffadb2ec4;hb=2ecd65dbcc1388bb2dfe6425e6ef1b2e3f45c4ac;hp=55d643262e15b4d4201359a0a6f0c01d515c9871;hpb=4efbd5e75ff51c4104be8c5f35dbabb65f51461f;p=helm.git diff --git a/helm/matita/library/nat/primes1.ma b/helm/matita/library/nat/primes1.ma index 55d643262..3df3922a4 100644 --- a/helm/matita/library/nat/primes1.ma +++ b/helm/matita/library/nat/primes1.ma @@ -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