Forbidden interval chain

import Mathlib.Algebra.Order.Archimedean.Real.Basic

section
namespace D1Bound5


theorem _root_.D1Bound5.forbidden_interval_chain {R : Type*} [LinearOrder R]
    (lower upper : ℕ → R) (x : R)
    (hstart : lower 0 ≤ x)
    (hoverlap : ∀ n, lower (n+1) ≤ upper n)
    (hexcluded : ∀ n, ¬ (lower n ≤ x ∧ x ≤ upper n))
    (hunbounded : ∃ n, x < lower n) : False := by sorry







end D1Bound5
end