X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fprimes.ma;h=7c5df29f35151cebe5d3c6664368c8ee9f2ece73;hb=ddc80515997a3f56085c6234d4db326141e189aa;hp=c44caa7fef34bd19c77340b40a7d6111bcc85d1d;hpb=fc7af5f9ea2cd4a876b8babc6b691136799e3c87;p=helm.git

diff --git a/matita/matita/lib/arithmetics/primes.ma b/matita/matita/lib/arithmetics/primes.ma
index c44caa7fe..7c5df29f3 100644
--- a/matita/matita/lib/arithmetics/primes.ma
+++ b/matita/matita/lib/arithmetics/primes.ma
@@ -480,7 +480,7 @@ change with
 (let previous_prime ≝ (nth_prime n) in
  let upper_bound ≝ S previous_prime! in
  S previous_prime ≤ min upper_bound (S previous_prime) primeb)
-apply le_min_l
+@le_min_l
 qed.
 
 theorem lt_SO_nth_prime_n : ∀n:nat. 1 < nth_prime n.