simpa using habs
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ - 1 ≡ ↑↑k₂ [ZMOD ↑p]
⊢ ↑↑k₂ = 0
no goals