theorem fixture_inf_primes (n : ℕ) : ∃ p, n < p ∧ Nat.Prime p := Nat.exists_infinite_primes n.succ

theorem fixture_even_or_odd (n : ℕ) : Even n ∨ Odd n := Nat.even_or_odd n

theorem fixture_add_comm (a b : ℕ) : a + b = b + a := by omega

theorem flt_invariant_isIntegral (A B G : Type*) [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [SMulCommClass G A B] [Algebra.IsInvariant A B G] [Finite G] : Algebra.IsIntegral A B := Algebra.IsInvariant.isIntegral A B G

theorem no_coprime_sol (p q : ℕ) (hcop : Nat.Coprime p q) (h : p ^ 2 = 2 * q ^ 2) : False := by have hp : 2 ∣ p := two_dvd_of_dvd_sq p ⟨q ^ 2, h⟩ obtain ⟨k, rfl⟩ := hp ha...

theorem n4_add_four_not_prime (n : ℕ) (hn : 2 ≤ n) : ¬ Nat.Prime (n ^ 4 + 4) := by obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩ have hm : 1 ≤ m := b...

theorem dvd_norm {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsIntegrallyClosed A] [IsDomain B] [IsIntegrallyClosed B] [Module.Finite A B] [Module.IsTorsionFree A B] (b : B) (hb : b ≠ 0) : ∃ a : A, a ≠ 0 ∧ b ∣ algebraMap A B a := ⟨Algebra.intNorm A B b, Algebra.intNorm_ne_zero.mpr hb, Algebra.dvd_algebraMa...

theorem infinitude_of_primes (n : ℕ) : ∃ p, n < p ∧ Nat.Prime p := by obtain ⟨p, hp, hpN⟩ := prime_factor_exists (Nat.factorial n + 1) (by have ...

theorem brocard_factor (n m : ℕ) (h : Nat.factorial n + 1 = (m + 1) ^ 2) : m * (m + 2) = Nat.factorial n := by have e : (m + 1) ^ 2 = m * (m + 2) + 1 := by ring omega

theorem brocard_7 : Nat.factorial 7 + 1 = 71 ^ 2 := by decide