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

diff --git a/matita/matita/lib/arithmetics/primes.ma b/matita/matita/lib/arithmetics/primes.ma
index c8b2a25bf..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))).