Negative integer square floor obstruction trace zero

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

section
namespace D1Bound5








theorem _root_.D1Bound5.negative_integer_square_floor_obstruction_trace_zero {nu m k : ℤ}
    (hnu : 0 < nu) (hk : 0 ≤ k)
    (hlo : nu * k ^ 2 < -m) (hhi : -m < nu * (k + 1) ^ 2) :
    ¬ ∃ r : QuadInt 0 nu, r * r = (m : QuadInt 0 nu) := by sorry



namespace QuadInt









end QuadInt
end D1Bound5
end