.ma inclusions corrected/minimized

[helm.git] / helm / matita / library / nat / log.ma

diff --git a/helm/matita/library/nat/log.ma b/helm/matita/library/nat/log.ma
index e24c3031f7873767920d1c6934be5cc65981f715..301c0be8ef1dc689646af66e4321177c2cb5372f 100644 (file)
--- a/helm/matita/library/nat/log.ma
+++ b/helm/matita/library/nat/log.ma
@@ -15,8 +15,9 @@
 set "baseuri" "cic:/matita/nat/log".
 
 include "datatypes/constructors.ma".
-include "nat/primes.ma".
 include "nat/exp.ma".
+include "nat/lt_arith.ma".
+include "nat/primes.ma".
 
 (* this definition of log is based on pairs, with a remainder *)