proposition: Lemma sup_ub {E} : has_ubound E -> ubound E (sup E).
proof: Proof. move=> ubE; apply/ubP=> x x_in_E; move: (x) (x_in_E). by apply/ubP/sup_upper_bound=> //; split; first by exists x. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid