reverse_complexity lib restored

[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 c8b2a25bf4e5f9d05ac3fffc2b0305c9a23ae66a..62c0a0081af5ecadfade0e7b0bbaa1ff4a3b216a 100644 (file)
--- 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))).
@@ -311,7 +310,7 @@ qed.
 
 theorem prime_smallest_factor_n : ∀n. 1 < n → 
   prime (smallest_factor n).
-#n #lt1n (cut (0<n)) [/2/] #posn % /2/ #m #divmmin #lt1m
+#n #lt1n (cut (0<n)) [/2/] #posn % (* bug? *) [/2/] #m #divmmin #lt1m
 @le_to_le_to_eq
   [@divides_to_le // @lt_O_smallest_factor //
   |>smallest_factor_to_min // @true_to_le_min //