constructor
case h.right.left
x a : ℝ
ha : a ∈ Set.Ici x
⊢ a ∈ Set.Ico a (a + 1)
case h.right.left.left
x a : ℝ
ha : a ∈ Set.Ici x
⊢ a ≤ a

case h.right.left.right
x a : ℝ
ha : a ∈ Set.Ici x
⊢ a < a + 1