proposition: Lemma inf_adherent E (eps : R) : 0 < eps -> has_inf E -> exists2 e, E e & e < inf E + eps.
proof: Proof. move=> + /has_inf_supN supNE => /sup_adherent /(_ supNE)[e NEx egtsup]. exists (- e); first by case: NEx => x Ex <-{}; rewrite opprK. by rewrite ltrNl -mulN1r mulrDr !mulN1r opprK. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid