proposition: Lemma consec_last (ks : seq A) t1 t2 : uniq ks -> consec ks t1 t2 -> t2 \notin ks <-> exists ks', ks = rcons ks' t1.
proof: Proof. move=>U /andP [T]; rewrite nilp_hasPn => /hasPn H. case: (lastP ks) U H T=>[|xs x] //= {ks} + H. rewrite rcons_uniq slt_rcons mem_rcons inE negb_or !(eq_sym x). case/andP=>Nx Ux; case: ifP=>X; rewrite ?andbF ?andbT. - move=>Nt; split=>//; case=>ks' /rcons_inj [??]; subst ks' x. by rewrite (slt_memE Nt) in Nx. move/contra: (H x)=>/(_ erefl). rewrite eqslice_mem_uniq /=; last by rewrite rcons_uniq Nx. rewrite mem_rcons inE eqxx /= in_itv /= negb_and ltEnat /= -!sleNgt !sle_rcons (negbTE Nx) X /= eqxx /= orbF andbT (eq_sym x). case/orP=>[/negbTE->|/eqP->] /=. - by case/andP=>H1 /eqP->; split=>// _; exists xs. rewrite eqxx /= orbF => H1; split=>//; case=>ks' /rcons_inj [_ Ex]. by rewrite Ex H1 in Nx. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)