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

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