* Almost ready for release 0.99.1.

[helm.git] / matita / matita / lib / arithmetics / primes.ma

diff --git a/matita/matita/lib/arithmetics/primes.ma b/matita/matita/lib/arithmetics/primes.ma
index c44caa7fef34bd19c77340b40a7d6111bcc85d1d..7c5df29f35151cebe5d3c6664368c8ee9f2ece73 100644 (file)
--- 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.