From dbe1642d535ef1bc3f673b342a02daf861f4f438 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 27 Sep 2005 16:28:34 +0000 Subject: [PATCH] small error in nth_prime. --- helm/matita/library/nat/nth_prime.ma | 3 --- 1 file changed, 3 deletions(-) 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. -- 2.39.2