proposition: Lemma consecP_split (ks : seq A) t1 t2 : uniq ks -> t2 \in ks -> reflect (exists xs1 xs2, ks = xs1++t1::t2::xs2) (consec ks t1 t2).
proof: Proof. move=>U T2; apply: (iffP idP). - case/andP=>+ H; case/slt_splitL=>xs1 [xs2][E] N T1 T2'. rewrite {ks}E mem_cat /= inE (negbTE T2') eq_sym (negbTE N) /= in U T2 H *. case/in_split: T2=>ks3 [ks4][E T2'']; rewrite {xs2}E in U H *. by rewrite eqsl_oo_split // in H; move/nilP: H=>->; exists xs1, ks4. case=>xs1 [xs2] E; move: U; rewrite {ks}E in T2 *. rewrite cat_uniq /= inE !negb_or -!andbA (eq_sym t1 t2). case/and8P=>U1 U2 U3 U4 U5 U6 U7 U8. by rewrite /consec slt_splitR // eqsl_oo_split_consec=>//; rewrite eq_sym. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)