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

diff --git a/matita/library/nat/primes.ma b/matita/library/nat/primes.ma
index 30339d654..c5fe7bd29 100644
--- a/matita/library/nat/primes.ma
+++ b/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.