proposition: Lemma Rsup_isLub x0 E : has_sup E -> isLub E (supremum x0 E).
proof: Proof. have [-> [/set0P]|E0 hsE] := eqVneq E set0; first by rewrite eqxx. have [s [Es sE]] := Rcondcomplete hsE. split => x Ex; first by apply/ge_supremum_Nmem=> //; exact: Rsupremums_neq0. rewrite /supremum (negbTE E0); case: xgetP => /=. by move=> _ -> [_ EsE]; apply/EsE. by have [y Ey /(_ y)] := Rsupremums_neq0 hsE. 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