From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 2 Oct 2006 15:15:31 +0000 (+0000)
Subject: removed a pointless call to auto
X-Git-Tag: 0.4.95@7852~958
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fd972f2c23de4c32d1335fb2b27e21854c6eb806;p=helm.git

removed a pointless call to auto
---

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