have h_ineq :
    ‖((X - C lamb).eval (q : ℂ))‖^2 > ((q : ℝ) - 1)^2  := by
  calc
    _ = ‖q - lamb‖^2 := by
      simp only [eval_sub, eval_X, eval_C, norm_eq_abs]
    _ = ‖(q : ℂ) - a - I*b‖^2 := by sorry
    _ = ‖(q : ℂ) - a‖^2 + ‖b‖^2 := by sorry
    _ = (q : ℝ)^2 - 2*‖a‖*q + ‖a‖^2 + ‖b‖^2 := by sorry
    _ > ((q : ℝ) - 1)^2 := by 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
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
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
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1