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