added a function to reorder the metasenv.

[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 9f32777b3cda096a75a2bc6d549301ded1c5bc61..e24c3031f7873767920d1c6934be5cc65981f715 100644 (file)
--- 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 ?.