]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/lib/arithmetics/nth_prime.ma
Non working parts of the library commented out.
[helm.git] / matita / matita / lib / arithmetics / nth_prime.ma
index 7b7c70bfe5cabfca704dce146034cb3ff1abad88..c973d0b12a272f74630310410960539b84acd8e1 100644 (file)
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* To be ported
 include "nat/primes.ma".
 include "nat/lt_arith.ma".
 
@@ -198,4 +199,4 @@ apply le_to_or_lt_eq.assumption.
 apply ex_m_le_n_nth_prime_m.
 simplify.unfold prime in H.elim H.assumption.
 qed.
-
+*)
\ No newline at end of file