proposition: Lemma max_sup {R : realType} x (E : set R) : (E `&` ubound E)%classic x -> sup E = x.
proof: Proof. case=> /= xE xubE; have nzE: nonempty E by exists x. apply/eqP; rewrite eq_le sup_le_ub //=. have : has_sup E by split; exists x. by move/sup_upper_bound/ubP; apply. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology