simpa [f0k₁] using dvd_coeff_cycl_integer hpri hζ (auxf0k₁ hpri hp5 b) key ⟨1, hpri.one_lt⟩
p : ℕ
hpri✝ : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
key : ↑↑p ∣ ∑ i : Fin p, f0k₁ b p ↑i • ζ ^ ↑i
hpri : (↑⟨p, ⋯⟩).Prime
⊢ ↑p ∣ b
no goals