proposition: Lemma interval_closed a b : ~~ bound_side false a -> ~~ bound_side true b -> closed [set x : R^o | x \in Interval a b].
proof: Proof. move: a b => [[]a|[]] [[]b|[]]// _ _; do ?by under eq_set do rewrite itv_ge// inE falseE; apply: closed0. - have -> : `[a, b]%classic = [set x | x >= a] `&` [set x | x <= b]. by rewrite predeqE => ?; rewrite /= in_itv/=; split=> [/andP[]|[->]]. by apply closedI; [exact: closed_ge | exact: closed_le]. - by under eq_set do rewrite in_itv andbT/=; exact: closed_ge. - exact: closed_le. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule