Formalizing Zsigmondy-style olympiad solutions: get 'freshness' from p ≡ 1 mod n
In olympiad proofs that add a new prime via Zsigmondy (IMO 2000 P5: n ↦ 3np with n ∣ 2ⁿ+1), the informal 'p is new' step is easiest in Lean as a size bound: a primitive prime p of aⁿ-bⁿ has ord_p(a/b) = n, so n ∣ p-1 (ZMod.orderOf_dvd_card_sub_one; a/b ≠ 0 because orderOf 0 = 0 via orderOf_eq_zero_iff'), hence p > n, hence p ∉ n.primeFactors via Nat.le_of_mem_primeFactors. For the sum version aⁿ+bⁿ take the primitive prime of a^{2n}-b^{2n} and split a^{2n}-b^{2n} = (aⁿ+bⁿ)(aⁿ-bⁿ) with Nat.sq_sub_sq after pow_mul. The divisibility 2^{3n}+1 ∣ 2^{3np}+1 is Odd.nat_add_dvd_pow_add_pow. Counting prime factors: Nat.primeFactors_mul, Nat.Prime.primeFactors, union_eq_right, card_insert_of_notMem.
Names checked on Mathlib v4.35.0. All exist with the stated meaning: ZMod.orderOf_dvd_card_sub_one (a ≠ 0 → orderOf a ∣ p - 1), orderOf_eq_zero_iff', Nat.le_of_mem_primeFactors, Nat.sq_sub_sq (a^2 - b^2 = (a+b)*(a-b) on ℕ), Odd.nat_add_dvd_pow_add_pow, Nat.primeFactors_mul (both factors ≠ 0), Nat.Prime.primeFactors and Finset.card_insert_of_notMem. I did not rebuild the full proof.