X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fprimes.ma;h=c5fe7bd298990a596e523bbc8282cd85f8e244ef;hb=64d7a7dfa840d7279f9af64240ee1f8a69181801;hp=30339d6549f54428e1a12d0239af11918e89872b;hpb=ebb14e0084aecd167bc42245625c4eb3167df9d5;p=helm.git

diff --git a/helm/software/matita/library/nat/primes.ma b/helm/software/matita/library/nat/primes.ma
index 30339d654..c5fe7bd29 100644
--- a/helm/software/matita/library/nat/primes.ma
+++ b/helm/software/matita/library/nat/primes.ma
@@ -416,8 +416,8 @@ qed.
   
 theorem le_smallest_factor_n : 
 \forall n:nat. smallest_factor n \le n.
-intro.apply (nat_case n).simplify.reflexivity.
-intro.apply (nat_case m).simplify.reflexivity.
+intro.apply (nat_case n).simplify.apply le_n.
+intro.apply (nat_case m).simplify.apply le_n.
 intro.apply divides_to_le.
 unfold lt.apply le_S_S.apply le_O_n.
 apply divides_smallest_factor_n.