X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Fnth_prime.ma;h=e174266e6884f41cfb4fe256cbe83294790096a4;hb=06a089726af079d5b2fe42ba78632565dad0eb3e;hp=4a054a3b4c5128bcde973194d4f7e86fd5c8a4b2;hpb=04e27500136c94e4f2ac072a5e4d330b75da35f0;p=helm.git

diff --git a/matita/library/nat/nth_prime.ma b/matita/library/nat/nth_prime.ma
index 4a054a3b4..e174266e6 100644
--- a/matita/library/nat/nth_prime.ma
+++ b/matita/library/nat/nth_prime.ma
@@ -77,7 +77,7 @@ match n with
     min_aux (upper_bound - (S previous_prime)) upper_bound primeb].
     
 (* it works, but nth_prime 4 takes already a few minutes -
-it must compute factorial of 7 ...
+it must compute factorial of 7 ...*)
 
 theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
 normalize.reflexivity.
@@ -89,6 +89,11 @@ qed.
 
 theorem example13 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
 normalize.reflexivity.
+qed.
+
+(*
+theorem example14 : nth_prime (S(S(S(S(S O))))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
+normalize.reflexivity.
 *) 
 
 theorem prime_nth_prime : \forall n:nat.prime (nth_prime n).