proposition: Lemma inf_lower_bound E : has_inf E -> lbound E (inf E).
proof: Proof. move=> /has_inf_supN /sup_upper_bound /ubP inflb; apply/lbP => x. by rewrite memNE => /inflb; rewrite lerNl. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid