Negative integer square floor obstruction trace one

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_one {nu m k : ℤ}
    (hd : 0 < 4 * nu - 1) (hk : 0 ≤ k)
    (hlo : (4 * nu - 1) * k ^ 2 < -m)
    (hhi : -m < (4 * nu - 1) * (k + 1) ^ 2) :
    ¬ ∃ r : QuadInt 1 nu, r * r = (m : QuadInt 1 nu) := by sorry

namespace QuadInt









end QuadInt
end D1Bound5
end