First attempt at using/simulating records with manifest types to encode

[helm.git] / matita / library / nat / primes.ma

diff --git a/matita/library/nat/primes.ma b/matita/library/nat/primes.ma
index 30339d6549f54428e1a12d0239af11918e89872b..c5fe7bd298990a596e523bbc8282cd85f8e244ef 100644 (file)
--- 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.