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.
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).
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).