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

diff --git a/matita/matita/lib/arithmetics/primes.ma b/matita/matita/lib/arithmetics/primes.ma
index 68e511e98..62c0a0081 100644
--- a/matita/matita/lib/arithmetics/primes.ma
+++ b/matita/matita/lib/arithmetics/primes.ma
@@ -310,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 //