proposition: Lemma itv_splitU1 b x : b <= BLeft x -> Interval b (BRight x) =i [predU1 x & Interval b (BLeft x)].
proof: Proof. move=> bx z; rewrite !inE/= !subitvE ?bnd_simp//= lt_neqAle. by case: (eqVneq z x) => [->|]//=; rewrite lexx bx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)