Quad Int — exists normalized root

import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Data.Int.Sqrt
import Mathlib.Tactic.Linarith
import Definitions.Def_D1Bound5_Coordinates_Definitions

section
namespace D1Bound5.QuadInt

variable {tau nu : ℤ}




theorem _root_.D1Bound5.QuadInt.exists_normalized_root {z : QuadInt tau nu} (hz : ∃ r, r*r = z) :
    ∃ r : QuadInt tau nu, r*r = z ∧ 0 ≤ 2*r.re+tau*r.im ∧
      (2*r.re+tau*r.im = 0 → 0 ≤ r.im) := by sorry





















end D1Bound5.QuadInt
end