sorry
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this : 0 ≤ (↑q - 1) ^ 2
g : ((↑q - 1) ^ 2).sqrt < (‖eval (↑q) (X - C lamb)‖ ^ 2).sqrt
⊢ ((↑q - 1) ^ 2).sqrt = ↑q - 1
no goals