## Notable Theorems #

- `Nat.exists_infinite_primes`: Euclid's theorem that there exist infinitely many prime numbers. This also appears as `Nat.not_bddAbove_setOf_prime` and `Nat.infinite_setOf_prime` (the latter in `Data.Nat.PrimeFin`).

source
theorem Nat.exists_infinite_primes (n : ℕ) :
∃ (p : ℕ), n ≤ p ∧ Prime p

Euclid's theorem on the infinitude of primes. Here given in the form: for every `n`, there exists a prime number `p ≥ n`.

source
theorem Nat.not_bddAbove_setOf_prime :
¬BddAbove {p : ℕ | Prime p}

A version of `Nat.exists_infinite_primes` using the `BddAbove` predicate.