examples of applyS

[helm.git] / matita / library / nat / nth_prime.ma

diff --git a/matita/library/nat/nth_prime.ma b/matita/library/nat/nth_prime.ma
index 4a054a3b4c5128bcde973194d4f7e86fd5c8a4b2..e174266e6884f41cfb4fe256cbe83294790096a4 100644 (file)
--- 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).