Quad Int — three le discriminant

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

section
namespace D1Bound5


theorem _root_.D1Bound5.QuadInt.three_le_discriminant {tau nu : ℤ}
    (hd : 0 < QuadInt.discriminant tau nu) :
    3 ≤ QuadInt.discriminant tau nu := by sorry








end D1Bound5
end