Positive integer square is integer

import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Data.Int.Sqrt
import Mathlib.Tactic.Linarith
import Definitions.Def_D1Bound5_Coordinates_Definitions

section
namespace D1Bound5

open QuadInt










theorem _root_.D1Bound5.positive_integer_square_is_integer {tau nu m : ℤ}
    (hd : 0 < discriminant tau nu) (hm : 0 < m)
    (hr : ∃ r : QuadInt tau nu, r*r = (m : QuadInt tau nu)) :
    ∃ n : ℤ, m = n^2 := by sorry

end D1Bound5
end