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

diff --git a/helm/matita/library/nat/log.ma b/helm/matita/library/nat/log.ma
index 9f32777b3..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 *)
 
@@ -73,8 +74,8 @@ rewrite < H3.rewrite > plus_n_O (m*(div n1 m)).
 rewrite < H2.
 rewrite > sym_times.
 rewrite < div_mod.reflexivity.
-intros.simplify.apply plus_n_O. 
 assumption.assumption.
+intros.simplify.apply plus_n_O. 
 qed.
 
 theorem plog_aux_to_exp: \forall p,n,m,q,r. O < m \to
@@ -134,6 +135,7 @@ match (plog_aux m1 (div ((exp m (S n1))*n) m) m) with
 cut div ((exp m (S n1))*n) m = (exp m n1)*n.
 rewrite > Hcut1.
 rewrite > H2 m1. simplify.reflexivity.
+apply le_S_S_to_le.assumption.
 (* div_exp *)
 change with div (m*(exp m n1)*n) m = (exp m n1)*n.
 rewrite > assoc_times.
@@ -144,7 +146,6 @@ apply divides_to_mod_O.
 assumption.
 simplify.rewrite > assoc_times.
 apply witness ? ? ((exp m n1)*n).reflexivity.
-apply le_S_S_to_le.assumption.
 qed.
 
 theorem plog_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
@@ -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.