From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 27 Sep 2005 16:28:34 +0000 (+0000)
Subject: small error in nth_prime.
X-Git-Tag: V_0_7_2_3~292
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dbe1642d535ef1bc3f673b342a02daf861f4f438;p=helm.git

small error in nth_prime.
---

diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma
index 1f3a57d7f..84407538d 100644
--- a/helm/matita/library/nat/nth_prime.ma
+++ b/helm/matita/library/nat/nth_prime.ma
@@ -110,7 +110,6 @@ cut S (nth_prime m)!-(S (nth_prime m)! - (S (nth_prime m))) = (S (nth_prime m)).
 rewrite > Hcut.exact smallest_factor_fact (nth_prime m).
 (* maybe we could factorize this proof *)
 apply plus_to_minus.
-apply le_minus_m.
 apply plus_minus_m_m.
 apply le_S_S.
 apply le_n_fact_n.
@@ -134,7 +133,6 @@ cut upper_bound - (upper_bound -(S previous_prime)) = (S previous_prime).
 rewrite < Hcut in \vdash (? % ?).
 apply le_min_aux.
 apply plus_to_minus.
-apply le_minus_m.
 apply plus_minus_m_m.
 apply le_S_S.
 apply le_n_fact_n.
@@ -177,7 +175,6 @@ apply lt_min_aux_to_false primeb upper_bound (upper_bound - (S previous_prime))
 cut S (nth_prime n)!-(S (nth_prime n)! - (S (nth_prime n))) = (S (nth_prime n)).
 rewrite > Hcut.assumption.
 apply plus_to_minus.
-apply le_minus_m.
 apply plus_minus_m_m.
 apply le_S_S.
 apply le_n_fact_n.