proposition: Lemma has_sup_half x b (i : itv_bound R) : (i < BSide b x)%O -> has_sup [set` Interval i (BSide b x)].
proof: Proof. move: b i => [] [[]y|[]]; rewrite ?bnd_simp => xy; split=> //; do 1?[ by exists ((x + y) / 2); rewrite !set_itvE/= addrC !(midf_le,midf_lt) //; exact: ltW | by exists (x - 1); rewrite !set_itvE/= !(ltrBlDr, lerBlDr, ltrDl,lerDl)]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets functions) HB(structures) reals ereal signed topology normedtype sequences