This file contains some results about prime numbers which depend on finiteness of sets.
A version of Nat.exists_infinite_primes using the Set.Infinite predicate.
If a, b are positive, the prime divisors of a * b are the union of those of a and b
a * b
The only prime divisor of positive prime power p^k is p itself