X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fnth_prime.ma;h=9d01e99f211e0b3a6e65cc7cb567c732aeff1c6e;hb=6423f1b6e3056883016598e454c55cab1004dfd2;hp=4a054a3b4c5128bcde973194d4f7e86fd5c8a4b2;hpb=ebb14e0084aecd167bc42245625c4eb3167df9d5;p=helm.git

diff --git a/helm/software/matita/library/nat/nth_prime.ma b/helm/software/matita/library/nat/nth_prime.ma
index 4a054a3b4..9d01e99f2 100644
--- a/helm/software/matita/library/nat/nth_prime.ma
+++ b/helm/software/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).
@@ -154,6 +159,17 @@ intros.apply (trans_lt O (S O)).
 unfold lt. apply le_n.apply lt_SO_nth_prime_n.
 qed.
 
+theorem lt_n_nth_prime_n : \forall n:nat. n \lt nth_prime n.
+intro.
+elim n
+  [apply lt_O_nth_prime_n
+  |apply (lt_to_le_to_lt ? (S (nth_prime n1)))
+    [unfold.apply le_S_S.assumption
+    |apply lt_nth_prime_n_nth_prime_Sn
+    ]
+  ]
+qed.
+
 theorem ex_m_le_n_nth_prime_m: 
 \forall n: nat. nth_prime O \le n \to 
 \exists m. nth_prime m \le n \land n < nth_prime (S m).