proposition: Lemma itv_splitUeq x a b : x \in Interval a b -> forall y, y \in Interval a b = [|| y \in Interval a (BLeft x), y == x | y \in Interval (BRight x) b].
proof: Proof. case/andP => ax xb y; rewrite (@itv_splitU (BLeft x)) ?ax ?ltW //. by congr orb; rewrite (@itv_splitU (BRight x)) ?bound_lexx // itv_xx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)