Growth quadratic negative

import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Algebra.Ring.Basic
import Mathlib.Algebra.Ring.Equiv
import Mathlib.Analysis.Complex.Norm
import Mathlib.Data.Finset.Card
import Mathlib.Data.Int.GCD
import Mathlib.LinearAlgebra.Dimension.Free
import Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
import Mathlib.NumberTheory.NumberField.Norm
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Mathlib.Tactic.Ring

section
open scoped NumberField
open Module

namespace D1Bound5








theorem _root_.D1Bound5.growth_quadratic_negative (A B C : ℝ) (hA : 3 ≤ A) (hAB : A ≤ B)
    (hBC : B ≤ C) (hC : C ≤ 2*A*B) :
    (A+B+C+1)^2+4-4*A*B*C < 0 := by sorry





end D1Bound5
end