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

diff --git a/helm/matita/library/nat/log.ma b/helm/matita/library/nat/log.ma
index 9f32777b3..e24c3031f 100644
--- a/helm/matita/library/nat/log.ma
+++ b/helm/matita/library/nat/log.ma
@@ -73,8 +73,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 +134,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 +145,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,7 +174,7 @@ apply lt_div_n_m_n.assumption.assumption.assumption.
 intros.
 change with (\lnot (mod n1 m = O)).
 rewrite > H4.
-(* META NOT FOUND !!! 
+(* META NOT FOUND !!!  
 rewrite > sym_eq. *)
 simplify.intro.
 apply not_eq_O_S m1 ?.