proposition: Lemma interval_right_unbounded_interior (X : set R) : is_interval X -> has_lbound X -> ~ has_ubound X -> X^° = [set r | inf X < r].
proof: Proof. move=> iX lX uX; rewrite eqEsubset; split; first exact: left_bounded_interior. rewrite -(open_subsetE _ (@open_gt _ _)) => r infXr. move/has_ubPn : uX => /(_ r)[y Xy yr]. have hiX : has_inf X by split => //; exists y. have /inf_adherent/(_ hiX)[e Xe] : 0 < r - inf X by rewrite subr_gt0. by rewrite addrCA subrr addr0 => er; apply: (iX e y); 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