proposition: Lemma itv_split1U b x : BRight x <= b -> Interval (BLeft x) b =i [predU1 x & Interval (BRight x) b].
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)