proposition: Corollary slice_uxxo s a b : a <= b -> &:s `]-oo, b] = &:s `]-oo, a] ++ &:s `]a, b].
proof: Proof. by move=>Hab; rewrite (slice_split _ false (x:=a)). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)