proposition: Corollary slice_split s (i : interval nat) b (x : nat) : x \in i -> &:s i = &:s (Interval i.1 (BSide b x)) ++ &:s (Interval (BSide b x) i.2).
proof: Proof. move=>Hx; apply: slice_split_bnd. case: i Hx=>[[l i|[]][r j|[]]] //=; rewrite in_itv /= ?andbT ?andbF // ?leBSide; case: b=>/=; rewrite ?implybF ?implybT //=. - by case/andP=>->/= /lteifW. - by case/andP=>/lteifW->. - by move/lteifW. by move/lteifW. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)