proposition: Lemma real_sup_adherent x0 E (eps : R) : (0 < eps) -> has_sup E -> exists2 e, E e & (supremum x0 E - eps) < e.
proof: Proof. move=> eps_gt0 supE; set m := _ - eps; apply: contrapT=> mNsmall. have : (ubound E) m. apply/ubP => y Ey. by have /negP := mNsmall (ex_intro2 _ _ y Ey _); rewrite -leNgt. have [_ /(_ m)] := Rsup_isLub x0 supE. move => m_big /m_big. by rewrite -subr_ge0 addrC addKr oppr_ge0 leNgt eps_gt0. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun Zwf Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def Rtrigo1 Reals mathcomp(all_ssreflect ssralg poly mxpoly ssrnum) HB(structures) mathcomp(boolp classical_sets) reals