proposition: Lemma ereal_supremums_neq0 S : supremums S !=set0.
proof: Proof. have [->|Snoo] := eqVneq S [set -oo]. by exists -oo; split; [rewrite ub_set1 |exact: lb_ub_refl]. have [->|S0] := eqVneq S set0. by exists -oo; exact: ereal_supremums_set0_ninfty. have [Spoo|Spoo] := pselect (S +oo). by exists +oo; split; [apply/ereal_ub_pinfty | apply/lbP => /= y /ubP; apply]. have [r Sr] : exists r, S r%:E. move: S0 => /set0P[] [r Sr| // |Snoo1]; first by exists r. apply/not_existsP => nS; move/negP : Snoo; apply. by apply/eqP; rewrite predeqE => -[] // r; split => // /nS. set U := fine_def r @` S. have [|] := eqVneq (ubound U) set0. rewrite -subset0 => U0; exists +oo. split; [exact/ereal_ub_pinfty | apply/lbP => /= -[r0 /ubP Sr0|//|]]. - suff : ubound U r0 by move/U0. by apply/ubP=> _ -[] [r1 Sr1 <-|//| /= _ <-]; rewrite -lee_fin; apply Sr0. - by move/ereal_ub_ninfty => [|]; by [move/eqP : S0|move/eqP : Snoo]. set u : R := sup U. exists u%:E; split; last first. apply/lbP=> -[r0 /ubP Sr0| |]. - rewrite lee_fin; apply/sup_le_ub; first by exists r, r%:E. by apply/ubP => _ -[[r2 ? <-| // | /= _ <-]]; rewrite -lee_fin; exact: Sr0. - by rewrite leey. - by move/ereal_ub_ninfty=> [|/eqP //]; [move/eqP : S0|rewrite (negbTE Snoo)]. apply/ubP => -[r0 Sr0|//|_]; last by rewrite leNye. rewrite lee_fin. suff : has_sup U by move/sup_upper_bound/ubP; apply; exists r0%:E. split; first by exists r0, r0%:E. exists u; apply/ubP => y; move=> [] y' Sy' <-{y}. have : has_sup U by split; [exists r, r%:E | exact/set0P]. move/sup_upper_bound/ubP; apply. by case: y' Sy' => [r1 /= Sr1 | // | /= _]; [exists r1%:E | exists r%:E]. 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