proposition: Lemma right_bounded_interior (R : realType) (X : set R) : has_ubound X -> X^° `<=` [set r | r < sup X].
proof: Proof. move=> uX r Xr; rewrite /mkset ltNge; apply/negP. rewrite le_eqVlt => /orP[/eqP supXr|]; last first. by apply/negP; rewrite -leNgt sup_ub //; exact: interior_subset. suff : ~ X^° (sup X) by rewrite supXr. case/nbhs_ballP => _/posnumP[e] supXeX. have [f XsupXf] : exists f : {posnum R}, X (sup X + f%:num). exists (e%:num / 2)%:pos; apply supXeX; rewrite /ball /= opprD addrA subrr. by rewrite sub0r normrN gtr0_norm // ltr_pdivrMr // ltr_pMr // ltr1n. have : sup X + f%:num <= sup X by apply sup_ub. by apply/negP; rewrite -ltNge; rewrite ltrDl. 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