proposition: Lemma interval_bounded_interior (X : set R) : is_interval X -> has_lbound X -> has_ubound X -> X^° = [set r | inf X < r < sup X].
proof: Proof. move=> iX bX aX; rewrite eqEsubset; split=> [r Xr|]. apply/andP; split; [exact: left_bounded_interior|exact: right_bounded_interior]. rewrite -open_subsetE; last exact: (@interval_open _ (BRight _) (BLeft _)). move=> r /andP[iXr rsX]. have [X0|/set0P X0] := eqVneq X set0. by move: (lt_trans iXr rsX); rewrite X0 inf_out ?sup_out ?ltxx // => - [[]]. have hiX : has_inf X by split. have /inf_adherent/(_ hiX)[e Xe] : 0 < r - inf X by rewrite subr_gt0. rewrite addrCA subrr addr0 => er. have hsX : has_sup X by split. have /sup_adherent/(_ hsX)[f Xf] : 0 < sup X - r by rewrite subr_gt0. by rewrite opprB addrCA subrr addr0 => rf; apply: (iX e f); rewrite ?ltW. 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