proposition: Lemma hasNub_ereal_sup (A : set R) : ~ has_ubound A -> A !=set0 -> ereal_sup (EFin @` A) = +oo%E.
proof: Proof. move=> + A0; apply: contra_notP => /eqP; rewrite -ltey => Aoo. exists (fine (ereal_sup (EFin @` A))) => x Ax. rewrite -lee_fin -(@fineK _ x%:E)// lee_fin fine_le//; last first. by apply: ereal_sup_ub => /=; exists x. rewrite fin_numE// -ltey Aoo andbT. apply/eqP => /ereal_sup_ninfty/(_ x%:E). by have /[swap] /[apply]: (EFin @` A) x%:E by exists x. 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