From fd972f2c23de4c32d1335fb2b27e21854c6eb806 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
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