proposition: Lemma ereal_sup_ninfty S : ereal_sup S = -oo <-> S `<=` [set -oo].
proof: Proof. split. by move=> supS [r /ereal_sup_ub | /ereal_sup_ub |//]; rewrite supS. move=> /(@subset_set1 _ S) [] ->; [exact: ereal_sup0|exact: ereal_sup1]. 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