X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fexp.ma;h=11d84f74ca7deb3b676007693f72b585c0547435;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=49e3bbd70f16a67399bacfa77d4d8001c2e231dd;hpb=fb94e5a71be508516514dfe50528ccfb3cd2da91;p=helm.git

diff --git a/helm/matita/library/nat/exp.ma b/helm/matita/library/nat/exp.ma
index 49e3bbd70..11d84f74c 100644
--- a/helm/matita/library/nat/exp.ma
+++ b/helm/matita/library/nat/exp.ma
@@ -48,14 +48,14 @@ rewrite < times_n_Sm.reflexivity.
 qed.
 
 theorem lt_O_exp: \forall n,m:nat. O < n \to O < n \sup m. 
-intros.elim m.simplify.apply le_n.
-simplify.rewrite > times_n_SO.
+intros.elim m.simplify.unfold lt.apply le_n.
+simplify.unfold lt.rewrite > times_n_SO.
 apply le_times.assumption.assumption.
 qed.
 
 theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < n \sup m.
-intros.elim m.simplify.reflexivity.
-simplify.
+intros.elim m.simplify.unfold lt.reflexivity.
+simplify.unfold lt.
 apply (trans_le ? ((S(S O))*(S n1))).
 simplify.
 rewrite < plus_n_Sm.apply le_S_S.apply le_S_S.
@@ -83,7 +83,7 @@ intros.apply eq_f.
 apply H1.
 (* esprimere inj_times senza S *)
 cut (\forall a,b:nat.O < n \to n*a=n*b \to a=b).
-apply Hcut.simplify. apply le_S_S_to_le. apply le_S. assumption.
+apply Hcut.simplify.unfold lt.apply le_S_S_to_le. apply le_S. assumption.
 assumption.
 intros 2.
 apply (nat_case n).