proposition: Lemma ereal_sup_ub S : ubound S (ereal_sup S).
proof: Proof. move=> y Sy; rewrite /ereal_sup /supremum ifF; last first. by apply/eqP; rewrite predeqE => /(_ y)[+ _]; exact. case: xgetP => /=; first by move=> _ -> -[] /ubP geS _; apply geS. by case: (ereal_supremums_neq0 S) => /= x0 Sx0; move/(_ x0). 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