Quad Int — root Candidate complete

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.rootCandidate_complete (hd : 0 < discriminant tau nu)
    {z : QuadInt tau nu} (hz : ∃ r, r*r = z) : rootCandidate z*rootCandidate z = z := by sorry













end D1Bound5.QuadInt
end