Ordinary height scalar envelope

import Mathlib.Algebra.Order.Floor.Semiring
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Tactic

section
namespace D1Bound5




theorem _root_.D1Bound5.ordinary_height_scalar_envelope (x z d p q h r u : ℝ)
    (hz : 0 ≤ z) (hq : 0 ≤ q)
    (hp : 2*x+r < p) (hp0 : 0 < 2*x+r)
    (hqh : q < x+h) (hxt : h-r < x)
    (hbound : z*(p-q) < (2*x+u)*p)
    (hd : d < (2/5 : ℝ)-x+2*z) :
    d < 7*x+(4*u+8*h-4*r)+
      (2*u*r+(4*u+8*h-4*r)*(h-r))/(x-(h-r))+(2/5 : ℝ) := by sorry



end D1Bound5
end