Quad Int — has Square Root iff

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

section
namespace D1Bound5.QuadInt

variable {tau nu : ℤ}


















theorem _root_.D1Bound5.QuadInt.hasSquareRoot_iff (hd : 0 < discriminant tau nu) (z : QuadInt tau nu) :
    hasSquareRoot z = true ↔ ∃ r : QuadInt tau nu, r*r = z := by sorry







end D1Bound5.QuadInt
end