theorem FltRegular.MayAssume.p_ne_three {a : ℤ} {b : ℤ} {c : ℤ} {n : ℕ} (hprod : a * b * c ≠ 0) (h : a ^ n + b ^ n = c ^ n) : n ≠ 3

theorem FltRegular.MayAssume.coprime {a : ℤ} {b : ℤ} {c : ℤ} {n : ℕ} (H : a ^ n + b ^ n = c ^ n) (hprod : a * b * c ≠ 0) : let d := Finset.gcd {a, b, c} id; (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ Finset.gcd {a / d, b / d, c / d} id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0

theorem FltRegular.p_dvd_c_of_ab_of_anegc {p : ℕ} {a : ℤ} {b : ℤ} {c : ℤ} (hpri : Nat.Prime p) (hp : p ≠ 3) (h : a ^ p + b ^ p = c ^ p) (hab : a ≡ b [ZMOD ↑p]) (hbc : b ≡ -c [ZMOD ↑p]) : ↑p ∣ c

theorem FltRegular.a_not_cong_b {p : ℕ} {a : ℤ} {b : ℤ} {c : ℤ} (hpri : Nat.Prime p) (hp5 : 5 ≤ p) (hprod : a * b * c ≠ 0) (h : a ^ p + b ^ p = c ^ p) (hgcd : Finset.gcd {a, b, c} id = 1) (caseI : ¬↑p ∣ a * b * c) : ∃ x y z, x ^ p + y ^ p = z ^ p ∧ Finset.gcd {x, y, z} id = 1 ∧ ¬x ≡ y [ZMOD ↑p] ∧ x * y * z ≠ 0 ∧ ¬↑p ∣ x * y * z