proposition: Lemma ub_ereal_sup_adherent S (e : R) : (0 < e)%R -> ereal_sup S \is a fin_num -> exists2 x, S x & (ereal_sup S - e%:E < x).
proof: Proof. move=> e0 Sr; have : ~ ubound S (ereal_sup S - e%:E). move/ub_ereal_sup; apply/negP. by rewrite -ltNge lte_subl_addr // lteDl // lte_fin. move/asboolP; rewrite asbool_neg; case/existsp_asboolPn => /= x. by rewrite not_implyE => -[? ?]; exists x => //; rewrite ltNge; apply/negP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(fsbigop cardinality set_interval) reals signed topology constructive_ereal