Integer scaled square floor obstruction

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

section
namespace D1Bound5




theorem _root_.D1Bound5.integer_scaled_square_floor_obstruction {scale m k : ℤ}
    (hscale : 0 < scale) (hk : 0 ≤ k)
    (hlo : scale * k ^ 2 < m) (hhi : m < scale * (k + 1) ^ 2) :
    ¬ ∃ n : ℤ, m = scale * n ^ 2 := by sorry







namespace QuadInt









end QuadInt
end D1Bound5
end