X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fnth_prime.ma;fp=helm%2Fmatita%2Flibrary%2Fnat%2Fnth_prime.ma;h=84407538d2a89236188a3f5dab7e5f111f13338a;hb=dbe1642d535ef1bc3f673b342a02daf861f4f438;hp=1f3a57d7fc5d2819fba32effdd2349b6e00e82fd;hpb=7273c698dd60c1a8a0f35b44376acb548c6a4a33;p=helm.git

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.