proposition: Lemma lb_ereal_inf_adherent S (e : R) : (0 < e)%R -> ereal_inf S \is a fin_num -> exists2 x, S x & (x < ereal_inf S + e%:E).
proof: Proof. move=> e0; rewrite fin_numN => /(ub_ereal_sup_adherent e0)[x []]. move=> y Sy <-; rewrite -lteNr => /lt_le_trans ex; exists y => //. by apply: ex; rewrite fin_num_oppeD// oppeK. 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