X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Flog.ma;h=51d0108d97d89d937a488c68d6fbb7bc1e0a5323;hb=2ecd65dbcc1388bb2dfe6425e6ef1b2e3f45c4ac;hp=e24c3031f7873767920d1c6934be5cc65981f715;hpb=78044035b4419e569df0d7f6a7f96fa32d21a19d;p=helm.git

diff --git a/helm/matita/library/nat/log.ma b/helm/matita/library/nat/log.ma
index e24c3031f..51d0108d9 100644
--- 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 *)
 
@@ -174,10 +175,10 @@ apply lt_div_n_m_n.assumption.assumption.assumption.
 intros.
 change with (\lnot (mod n1 m = O)).
 rewrite > H4.
-(* META NOT FOUND !!!  
+(* Andrea: META NOT FOUND !!!  
 rewrite > sym_eq. *)
 simplify.intro.
-apply not_eq_O_S m1 ?.
+apply not_eq_O_S m1.
 rewrite > H5.reflexivity.
 qed.