Normalized root perturbation

import Mathlib.Analysis.Complex.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring

section
namespace D1Bound5


theorem _root_.D1Bound5.normalized_root_perturbation (q : ℂ) (c rho : ℝ)
    (hc : 0 ≤ c) (hrho : 0 < rho) (hgap : rho < 1-c^2)
    (hRe : 0 ≤ q.re) (hq : ‖q^2-1‖ ≤ rho) :
    (1+c)*‖q-1‖ < rho := by sorry



end D1Bound5
end