proposition: Corollary slice_split_full s b (x : nat) : s = &:s (Interval -oo (BSide b x)) ++ &:s (Interval (BSide b x) +oo).
proof: Proof. by rewrite -[LHS](slice_uu s); apply: slice_split. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)