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
⊢ ↑q ^ 2 - 2 * ‖a‖ * ↑q + ‖a‖ ^ 2 + ‖b‖ ^ 2 > (↑q - 1) ^ 2
no goals