proposition: Lemma has_inf_half x b (i : itv_bound R) : (BSide b x < i)%O -> has_inf [set` Interval (BSide b x) i].
proof: Proof. move: b i => [] [[]y|[]]; rewrite ?bnd_simp => xy; do 1?[ by split=> //; exists ((x + y) / 2); rewrite !set_itvE/= !(midf_le,midf_lt) //; exact: ltW | by split => //; exists (x + 1); rewrite !set_itvE/= !(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