proposition: Lemma has_supPn {E} : E !=set0 -> ~ has_sup E <-> (forall x, exists2 y, E y & x < y).
proof: Proof. move=> nzE; split=> [/asboolPn|/has_ubPn h [_]] //. by rewrite asbool_and (asboolT nzE) /= => /asboolP/has_ubPn. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid