Quad Int — discriminant le four bound

import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Tactic.Linarith
import Definitions.Def_D1Bound5_Coordinates_Definitions

section
namespace D1Bound5



namespace QuadInt

variable {tau nu : ℤ}
















theorem _root_.D1Bound5.QuadInt.discriminant_le_four_bound (hd : 0 < discriminant tau nu)
    {z : QuadInt tau nu} {M : ℤ} (hM : z.norm ≤ M) (hy : z.im ≠ 0) :
    discriminant tau nu ≤ 4*M := by sorry

end QuadInt
end D1Bound5
end