]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/library/nat/nth_prime.ma
.ma inclusions corrected/minimized
[helm.git] / helm / matita / library / nat / nth_prime.ma
index ee21195dc10bd823f4a96b8998a87ad99f6bb562..37c60b4057713ac77ddf68e638b2279db7f235a9 100644 (file)
@@ -15,6 +15,7 @@
 set "baseuri" "cic:/matita/nat/nth_prime".
 
 include "nat/primes.ma".
+include "nat/lt_arith.ma".
 
 (* upper bound by Bertrand's conjecture. *)
 (* Too difficult to prove.