X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fexp.ma;h=e40844e3f9b837a20226e0619780267b816bf763;hb=69c5a60dfa385a3d0e270ed38eb0d970366792c5;hp=11d84f74ca7deb3b676007693f72b585c0547435;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/matita/library/nat/exp.ma b/helm/software/matita/library/nat/exp.ma
index 11d84f74c..e40844e3f 100644
--- a/helm/software/matita/library/nat/exp.ma
+++ b/helm/software/matita/library/nat/exp.ma
@@ -54,7 +54,7 @@ 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.unfold lt.reflexivity.
+intros.elim m.simplify.unfold lt.apply le_n.
 simplify.unfold lt.
 apply (trans_le ? ((S(S O))*(S n1))).
 simplify.