X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Ffactorization.ma;h=fc9352e12395cbb117af7054f01b17bc41d1c38d;hb=fd972f2c23de4c32d1335fb2b27e21854c6eb806;hp=4c8de0f51ff3e112205dda4c97d26ae1b9939bca;hpb=c0b3eeafbeea89d16f0615d07ddfe38f2ce10219;p=helm.git

diff --git a/matita/library/nat/factorization.ma b/matita/library/nat/factorization.ma
index 4c8de0f51..fc9352e12 100644
--- a/matita/library/nat/factorization.ma
+++ b/matita/library/nat/factorization.ma
@@ -126,20 +126,13 @@ cut (r \mod (nth_prime (max_prime_factor n)) \neq O);
     ]
   ].
 *)  
-cut (n=r*(nth_prime p)\sup(q));
-  [letin www \def le.letin www1 \def divides.
-   auto.
-(*
 apply (le_to_or_lt_eq (max_prime_factor r)  (max_prime_factor n)).
 apply divides_to_max_prime_factor.
 assumption.assumption.
 apply (witness r n ((nth_prime p) \sup q)).
-*)
- |
 rewrite < sym_times.
 apply (p_ord_aux_to_exp n n ? q r).
 apply lt_O_nth_prime_n.assumption.
-]
 qed.
 
 theorem p_ord_to_lt_max_prime_factor1: \forall n,p,q,r. O < n \to