-- Infinitude of the prime natural numbers
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.NumberTheory.Infinitude
import Prime
import Cardinal.Finite

theorem primes.subset_naturals
  shows (primes ⊆ ℕ)
proof
  intros p hp
  obtain ⟨hpNatural, hpPrime⟩ := primes.membership.forward with hp
  exact hpNatural

theorem primes.order_unbounded (n : Nat)
  shows ∃ p ∈ primes, n < p
proof
  obtain ⟨p, hpPrime, hnLessP⟩ := Euclid.larger_prime at n with assumption
  witness p
  constructor
  . apply primes.contains at p
    exact hpPrime
  . exact hnLessP

-- The set-level corollary lives apart from the elementary number theory, so
-- prime development and computation need not load the cardinality and
-- function library to state and prove Euclid's theorem.
theorem primes.infinite
  shows ¬Finite(primes)
proof
  exact infinite.of_unbounded_naturals with primes.subset_naturals, primes.order_unbounded