From e3396c6c9064039ed4330161ba8947217e220366 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 2 Oct 2006 15:15:31 +0000 Subject: [PATCH] removed a pointless call to auto --- helm/software/matita/library/nat/factorization.ma | 7 ------- 1 file changed, 7 deletions(-) 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 -- 2.39.2