X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fprimes.ma;h=68e511e982617f293eedfc320aaa6be1ec888447;hb=1efc4c2c7be1e4aff0ccccabf905d45795b3865f;hp=c44caa7fef34bd19c77340b40a7d6111bcc85d1d;hpb=b4681c749d6e8812fe86d5a9adbf4d4acbc3df06;p=helm.git

diff --git a/matita/matita/lib/arithmetics/primes.ma b/matita/matita/lib/arithmetics/primes.ma
index c44caa7fe..68e511e98 100644
--- a/matita/matita/lib/arithmetics/primes.ma
+++ b/matita/matita/lib/arithmetics/primes.ma
@@ -247,8 +247,7 @@ qed.
 
 (* smallest factor *)
 definition smallest_factor : nat → nat ≝
-λn:nat. if_then_else ? (leb n 1) n
-  (min n 2 (λm.(eqb (n \mod m) O))).
+λn:nat. if leb n 1 then n else min n 2 (λm.(eqb (n \mod m) O)).
 
 theorem smallest_factor_to_min : ∀n. 1 < n → 
 smallest_factor n = (min n 2 (λm.(eqb (n \mod m) O))).
@@ -439,9 +438,9 @@ let rec nth_prime n ≝ match n with
     min upper_bound (S previous_prime) primeb].
 
 lemma nth_primeS: ∀n.nth_prime (S n) = 
-  let previous_prime ≝ nth_prime n in
+   (let previous_prime ≝ nth_prime n in
     let upper_bound ≝ S previous_prime! in
-    min upper_bound (S previous_prime) primeb.
+    min upper_bound (S previous_prime) primeb).
 // qed.
     
 (* it works *)
@@ -480,7 +479,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.