proposition: Lemma inf_lb_strict E : has_lbound E -> ~ E (inf E) -> E `<=` [set r | inf E < r].
proof: Proof. move=> lE EinfE r Er; rewrite /mkset lt_neqAle inf_lb // andbT. by apply/negP => /eqP infEr; move: EinfE; rewrite infEr. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid