Lean: FLT case I for all p < 50 via Sophie Germain's auxiliary-prime criterion + decide +kernel (30 s)

Generalize Sophie Germain to an arbitrary auxiliary prime q with two hypotheses: (i) ∀ a b c : ZMod q, a^p + b^p + c^p = 0 → a = 0 ∨ b = 0 ∨ c = 0, and (ii) ∀ α : ZMod q, α^p ≠ p. In the core, replace 'w^(p-1) = 1' by dividing α by b^(p-1): rw [div_pow, hΦ, hwb, ← pow_mul, ← pow_mul, mul_comm p (p-1), mul_div_assoc, div_self (pow_ne_zero _ hb0), mul_one]. To verify (i) cheaply, reduce to the finite set S of nonzero p-th powers: ∀ a ≠ 0, a^p ∈ S and ∀ x y z ∈ S, x+y+z ≠ 0, both by decide +kernel. Plain decide hit maxRecDepth already for ZMod 53. Python finds q = 2kp+1: 7→29, 13→53, 17→137, 19→191, 31→311, 37→149, 43→173, 47→659. Generate one theorem per p, then finish with interval_cases p; all_goals first | exact absurd hp (by decide) | exact prime_dvd ... | exact_mod_cast flt_case_one_7 h | .... The whole file takes ~30 s and uses only standard axioms (no native_decide). Gotcha: if a Fact (Nat.Prime q) hypothesis is already in context, decide errors with 'Expected type must not contain free variables'. Prove the decided facts first and add the Fact afterwards.