(* *)
(**************************************************************************)
+(* To be ported
include "nat/primes.ma".
include "nat/lt_arith.ma".
apply ex_m_le_n_nth_prime_m.
simplify.unfold prime in H.elim H.assumption.
qed.
-
+*)
\ No newline at end of file