theorem C05S03.two_le {m : ℕ} (h0 : m ≠ 0) (h1 : m ≠ 1) : 2 ≤ m

theorem C05S03.exists_prime_factor {n : ℕ} (h : 2 ≤ n) : ∃ (p : ℕ), Nat.Prime p ∧ p ∣ n

theorem C05S03.primes_infinite (n : ℕ) : ∃ p > n, Nat.Prime p

theorem Nat.Prime.eq_of_dvd_of_prime {p : ℕ} {q : ℕ} (prime_p : Nat.Prime p) (prime_q : Nat.Prime q) (h : p ∣ q) : p = q

theorem C05S03.mem_of_dvd_prod_primes {s : Finset ℕ} {p : ℕ} (prime_p : Nat.Prime p) : (∀ n ∈ s, Nat.Prime n) → p ∣ ∏ n ∈ s, n → p ∈ s

theorem C05S03.primes_infinite' (s : Finset ℕ) : ∃ (p : ℕ), Nat.Prime p ∧ p ∉ s

theorem C05S03.bounded_of_ex_finset (Q : ℕ → Prop) : (∃ (s : Finset ℕ), ∀ (k : ℕ), Q k → k ∈ s) → ∃ (n : ℕ), ∀ (k : ℕ), Q k → k < n

theorem C05S03.ex_finset_of_bounded (Q : ℕ → Prop) [DecidablePred Q] : (∃ (n : ℕ), ∀ (k : ℕ), Q k → k ≤ n) → ∃ (s : Finset ℕ), ∀ (k : ℕ), Q k ↔ k ∈ s

theorem C05S03.mod_4_eq_3_or_mod_4_eq_3 {m : ℕ} {n : ℕ} (h : m * n % 4 = 3) : m % 4 = 3 ∨ n % 4 = 3

theorem C05S03.two_le_of_mod_4_eq_3 {n : ℕ} (h : n % 4 = 3) : 2 ≤ n

theorem C05S03.aux {m : ℕ} {n : ℕ} (h₀ : m ∣ n) (h₁ : 2 ≤ m) (h₂ : m < n) : n / m ∣ n ∧ n / m < n

theorem C05S03.exists_prime_factor_mod_4_eq_3 {n : ℕ} (h : n % 4 = 3) : ∃ (p : ℕ), Nat.Prime p ∧ p ∣ n ∧ p % 4 = 3

theorem C05S03.primes_mod_4_eq_3_infinite (n : ℕ) : ∃ p > n, Nat.Prime p ∧ p % 4 = 3