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