X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fnth_prime.ma;fp=helm%2Fmatita%2Flibrary%2Fnat%2Fnth_prime.ma;h=0b8f2bbe207f38580c466e45152f7cffc88cbbb2;hb=b8c6dd0220fba9ebed2d51d5808790b5949177ea;hp=37c60b4057713ac77ddf68e638b2279db7f235a9;hpb=c328a3c15e865515a56d1c1d6d0c2619245a60a0;p=helm.git

diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma
index 37c60b405..0b8f2bbe2 100644
--- a/helm/matita/library/nat/nth_prime.ma
+++ b/helm/matita/library/nat/nth_prime.ma
@@ -43,7 +43,7 @@ n < smallest_factor (S (fact n)).
 intros.
 apply not_le_to_lt.
 change with smallest_factor (S (fact n)) \le n \to False.intro.
-apply not_divides_S_fact n (smallest_factor(S (fact n))) ? ?.
+apply not_divides_S_fact n (smallest_factor(S (fact n))).
 apply lt_SO_smallest_factor.
 simplify.apply le_S_S.apply le_SO_fact.
 assumption.