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

diff --git a/helm/software/matita/library/nat/factorization.ma b/helm/software/matita/library/nat/factorization.ma
index 4c8de0f51..fc9352e12 100644
--- a/helm/software/matita/library/nat/factorization.ma
+++ b/helm/software/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