theorem comp_apply {α β γ : Type} (f : β → γ) (g : α → β) (x : α) : (f ∘ g) x = f (g x) := rfl

theorem modus_ponens {p q : Prop} (hp : p) (hpq : p → q) : q := hpq hp

theorem true_intro : True := trivial

theorem or_self_idem (p : Prop) : (p ∨ p) ↔ p := Iff.intro (fun h => h.elim id id) Or.inl

theorem and_self_idem (p : Prop) : (p ∧ p) ↔ p := by tauto

-- The only solution to xᵃ = yᵇ + 1 with x,y,a,b > 1 is 3² = 2³ + 1. theorem catalan_conjecture (x y a b : ℕ) (hx : 1 < x) (hy : 1 < y) (ha : 1 < a) (hb : 1 < b) (h : x ^ a = y ^ b + 1) : x = 3 ∧ a = 2 ∧ y = 2 ∧ b = 3 := sorry

/-- Fermat's Last Theorem is true -/ theorem Wiles_Taylor_Wiles : FermatLastTheorem := by -- Suppose Fermat's Last Theorem is false by_contra h -- then there exists a Frey package obtain ⟨P : FreyPackage⟩ := FreyPackage.of_not_FermatLastTheorem h -- but there is no Frey package exact P.false

-- If aˣ + bʸ = cᶜ with x, y, z > 2, then a, b, c share a common prime factor. theorem beal (a b c x y z : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hx : 2 < x) (hy : 2 < y) (hz : 2 < z) (h : a ^ x + b ^ y = c ^ z) : ∃ p : ℕ, Nat.Prime p ∧ p ∣ a ∧ p ∣ b ∧ p ∣ c :=

-- There is always a prime between n² and (n+1)² for every positive n. theorem legendre (n : ℕ) (hn : 0 < n) : ∃ p : ℕ, n^2 < p ∧ p < (n + 1)^2 ∧ Nat.Prime p :=

-- Every even integer greater than 2 is the sum of two primes. theorem goldbach (n : ℕ) (hn : 2 < n) (heven : Even n) : ∃ p q : ℕ, Nat.Prime p ∧ Nat.Prime q ∧ p + q = n :=