rw[Set.mem_Ici] at ha
case h.right.right
x a : ℝ
ha : a ∈ Set.Ici x
y : ℝ
hy : y ∈ Set.Ico a (a + 1)
⊢ y ∈ Set.Ici x
case h.right.right
x a : ℝ
ha : x ≤ a
y : ℝ
hy : y ∈ Set.Ico a (a + 1)
⊢ y ∈ Set.Ici x