Frontier quadratic interval exclusion

import Mathlib.Data.Real.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.GCongr
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring

section
namespace D1Bound5










theorem _root_.D1Bound5.frontier_quadratic_interval_exclusion (a b c lo hi x : ℝ)
    (ha : 0 ≤ a) (hlo : lo < x) (hhi : x ≤ hi)
    (hql : a*lo^2+b*lo+c < 0) (hqh : a*hi^2+b*hi+c < 0)
    (hqx : 0 ≤ a*x^2+b*x+c) : False := by sorry

end D1Bound5
end