proposition: Lemma consecP_last ks t1 t2 : uniq ks -> t2 \notin ks -> reflect (exists xs, ks = rcons xs t1) (consec ks t1 t2).
proof: Proof. move=>U T2; apply: (iffP idP). - by move/consec_last: T2; apply. case=>xs E; rewrite E /consec rcons_uniq mem_rcons inE negb_or eq_sym in U T2 *. case/andP: U T2=>T1 U /andP [N T2]. rewrite slt_rcons (negbTE T2) (negbTE T1) N eq_refl /= nilp_hasPn. rewrite -all_predC; apply/allP=>x /=; apply: contraTeq=>_. rewrite eqslice_mem_uniq; last by rewrite rcons_uniq T1. rewrite mem_rcons inE in_itv /= ltEnat /= !negb_and negb_or -!sleNgt !sle_rcons (eq_sym x) eqxx orbF T1 (negbTE T2) (negbTE N) /= andbC orbCA orbb. case: ifP=>/= _; last by rewrite orbN. by rewrite orbF sleNgt; apply: contra T1; exact: slt_memE. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)