constructor
case h.right.left
x a : ℝ
ha : a ∈ Set.Iio x
⊢ a ∈ Set.Ioc (a - 1) a
case h.right.left.left
x a : ℝ
ha : a ∈ Set.Iio x
⊢ a - 1 < a

case h.right.left.right
x a : ℝ
ha : a ∈ Set.Iio x
⊢ a ≤ a