proposition: Lemma inf_lb E : has_lbound E -> lbound E (inf E).
proof: Proof. by move/has_lb_ubN/sup_ub/ub_lbN; rewrite setNK. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid