proposition: Lemma sup_upper_bound {R : realType} (E : set R): has_sup E -> ubound E (sup E).
proof: Proof. exact: sup_upper_bound_subdef. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid