proposition: Lemma ereal_sup_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality) (S : {compare (0 : \bar R) & xnz & xr} -> Prop) (r := ereal_sup_reality_subdef xnz xr) : Signed.spec 0 ?=0 r (ereal_sup [set x%:num | x in S]%classic).
proof: Proof. rewrite {}/r; move: xr S => [[[]|]|] S /=; do ?[by apply: ub_ereal_sup => _ [? _ <-] |by case: ereal_sup => [s||]; rewrite ?leey ?leNye// !lee_fin -realE num_real]. 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