constructor
case h
a : ℝ
ha : 0 ≤ a
⊢ IsCompact (Icc (-a) a) ∧ (Icc (-a) a)ᶜ ⊆ Ioi a ∪ Iio (-a)
case h.left
a : ℝ
ha : 0 ≤ a
⊢ IsCompact (Icc (-a) a)

case h.right
a : ℝ
ha : 0 ≤ a
⊢ (Icc (-a) a)ᶜ ⊆ Ioi a ∪ Iio (-a)