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=200ccba5a9086b0ca2a940c7f19ae0964bb8402c;hb=ab44166935d77276c04fcce50aa8281292776e29;hp=8035d49ddba64dcb5d207ab2e4c9179d477d4d2c;hpb=7efb15b93cf42eae8b34a12a327ee7213c1dbecc;p=helm.git

diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma
index 8035d49dd..200ccba5a 100644
--- a/helm/matita/library/nat/nth_prime.ma
+++ b/helm/matita/library/nat/nth_prime.ma
@@ -62,7 +62,7 @@ apply ex_intro nat ? (smallest_factor (S (fact (S n1)))).
 split.split.
 apply smallest_factor_fact.
 apply le_smallest_factor_n.
-(* ancora hint non lo trova *)
+(* Andrea: ancora hint non lo trova *)
 apply prime_smallest_factor_n.
 change with (S(S O)) \le S (fact (S n1)).
 apply le_S.apply le_SSO_fact.
@@ -98,7 +98,6 @@ apply nat_case n.
 change with prime (S(S O)).
 apply primeb_to_Prop (S(S O)).
 intro.
-(* ammirare la resa del letin !! *)
 change with
 let previous_prime \def (nth_prime m) in
 let upper_bound \def S (fact previous_prime) in