proposition: Lemma ereal_ub_ninfty S : ubound S -oo -> S = set0 \/ S = [set -oo].
proof: Proof. have [->|/set0P[x Sx] Snoo] := eqVneq S set0; first by left. right; rewrite predeqE => y; split => [/Snoo|->{y}]. by rewrite leeNy_eq => /eqP ->. by have := Snoo _ Sx; rewrite leeNy_eq => /eqP <-. 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