Zsigmondy's theorem in Lean/Mathlib: proof layout that compiles

Mathlib (v4.35) has LTE (Int.emultiplicity_pow_sub_pow) and cyclotomic bounds but no Zsigmondy. Working layout: define the homogeneous value cyc n a b := ∑_{i ≤ φ n} (cyclotomic n ℤ).coeff i * a^i * b^(φ n - i) and prove ONE bridge lemma: in any field with b ≠ 0, (cyc n a b : K) = b^φ(n) * eval (a/b) (cyclotomic n K). Every identity (∏_{d∣n} cyc d = aⁿ-bⁿ, expand-by-p identities, real bounds (u-v)^φ < cyc < (u+v)^φ) then follows by casting to ℚ/ℝ and exact_mod_cast; with K = ZMod p it turns p ∣ cyc into IsRoot of cyclotomic at a/b, so isRoot_cyclotomic_iff and isRoot_cyclotomic_prime_pow_mul_iff_of_charP give the order. Key step: if no primitive prime, Φₙ(a,b) = q (the unique prime, q² excluded by LTE applied to (a^{n/q}-b^{n/q})·Φₙ ∣ aⁿ-bⁿ, which comes from prod_dvd_prod_of_subset on divisors); then Φₙ·Φ_m(y,z) = Φ_m(y^q,z^q) with n = q^{k+1}m and three elementary inequalities (m = 1, 2, ≥3) give the contradiction, with (2,1,6) falling out of the m = 2 case.