proposition: Corollary eqsl_oo_nil_split t1 t2 (s s2 : seq A) : t1 != t2 -> t2 \notin s -> &=(t1::s++t2::s2) `]t1, t2[ = s.
proof: Proof. move=>N X2. by rewrite -(cat0s (_ :: _ ++ _)); apply: eqsl_oo_split. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)