proposition: Lemma ereal_supy S : S +oo -> ereal_sup S = +oo.
proof: Proof. by move=> Soo; apply/eqP; rewrite eq_le leey/=; exact: ereal_sup_ub. 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