small error in nth_prime.

diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma
index 1f3a57d7fc5d2819fba32effdd2349b6e00e82fd..84407538d2a89236188a3f5dab7e5f111f13338a 100644 (file)
--- 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.