proposition: Lemma sup_adherent {R : realType} (E : set R) (eps : R) : 0 < eps -> has_sup E -> exists2 e : R, E e & (sup E - eps) < e.
proof: Proof. exact: sup_adherent_subdef. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid