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