proposition: Corollary eqsl_uxou (ks : seq A) t : ks = &=ks `]-oo, t] ++ &=ks `]t, +oo[.
proof: Proof. by exact: eqslice_split_full. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)