proposition: Lemma ub_ereal_sup S M : ubound S M -> ereal_sup S <= M.
proof: Proof. rewrite /ereal_sup /supremum; case: ifPn => [/eqP ->|]; first by rewrite leNye. - by move=> _ SM; case: xgetP => [_ -> [_]| _] /=; [exact |rewrite leNye]. 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