Quad Int — floor Obstruction Bool sound

import Mathlib.Algebra.Order.Ring.Abs
import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Data.Int.Sqrt
import Mathlib.Tactic.Linarith
import Definitions.Def_D1Bound5_Coordinates_Definitions
import Definitions.Def_D1Bound5_QuadSquareFloorObstruction_Definitions

section
namespace D1Bound5











namespace QuadInt








theorem _root_.D1Bound5.QuadInt.floorObstructionBool_sound {tau nu : ℤ}
    (hd : 0 < discriminant tau nu) {z : QuadInt tau nu} {k : ℕ}
    (h : floorObstructionBool z k = true) :
    ¬ ∃ r : QuadInt tau nu, r * r = z := by sorry

end QuadInt
end D1Bound5
end