proposition: Lemma has_ub_lbN E : has_ubound E <-> has_lbound (-%R @` E).
proof: Proof. rewrite has_lb_ubN image_comp /comp /=. by under eq_fun do rewrite opprK; rewrite image_id. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid