proposition: Lemma sup_ub_strict E : has_ubound E -> ~ E (sup E) -> E `<=` [set r | r < sup E].
proof: Proof. move=> ubE EsupE r Er; rewrite /mkset lt_neqAle sup_ub // andbT. by apply/negP => /eqP supEr; move: EsupE; rewrite -supEr. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid