X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Ffactorization.ma;h=85351c06d47ac9b63e5d4a94964d7d6e56f97a9c;hb=06a089726af079d5b2fe42ba78632565dad0eb3e;hp=d0036e4a1fcc147add9d888f359ee80c090ccb09;hpb=94983be5804a0ecbd14b43fe3b7475443bc8c804;p=helm.git

diff --git a/matita/library/nat/factorization.ma b/matita/library/nat/factorization.ma
index d0036e4a1..85351c06d 100644
--- a/matita/library/nat/factorization.ma
+++ b/matita/library/nat/factorization.ma
@@ -52,7 +52,7 @@ intros; apply divides_b_true_to_divides;
         apply (trans_lt ? (S O));
         [ unfold lt; apply le_n;
         | assumption; ] *) ] ]
-  | letin x \def prime. auto new.
+  | auto. 
     (* 
     apply prime_to_nth_prime;
     apply prime_smallest_factor_n;
@@ -70,8 +70,8 @@ apply divides_to_divides_b_true.
 cut (prime (nth_prime (max_prime_factor n))).
 apply lt_O_nth_prime_n.apply prime_nth_prime.
 cut (nth_prime (max_prime_factor n) \divides n).
-auto new.
-auto new.
+auto.
+auto.
 (*
   [ apply (transitive_divides ? n);
     [ apply divides_max_prime_factor_n.