From fd972f2c23de4c32d1335fb2b27e21854c6eb806 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 --- matita/library/nat/factorization.ma | 7 ------- 1 file changed, 7 deletions(-) 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 -- 2.39.2