proposition: Lemma supremum_pinfty S x0 : S +oo -> supremum x0 S = +oo.
proof: Proof. move=> Spoo; rewrite /supremum ifF; last by apply/eqP => S0; rewrite S0 in Spoo. have sSoo : supremums S +oo. split; first exact: ereal_ub_pinfty. by move=> /= y /(_ _ Spoo); rewrite leye_eq => /eqP ->. case: xgetP. by move=> _ -> sSxget; move: (is_subset1_supremums sSoo sSxget). by move/(_ +oo) => gSoo; exfalso; apply gSoo => {gSoo}. 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