proposition: Lemma slice_decompose s l r x y : &:s (Interval (BSide l x) (BSide r y)) = &:(&:s (Interval -oo (BSide r y))) (Interval (BSide l x) +oo).
proof: Proof. by rewrite /slice /= drop0 take_size. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)