proposition: Lemma consecP_lastE y ks t1 t2 : uniq ks -> t2 \notin ks -> consec ks t1 t2 = (t1 \in ks) && (t1 == last y ks).
proof: Proof. move=>U T2; case: consecP_last=>//. - by case=>xs ->; rewrite mem_rcons last_rcons inE eq_refl. move=>H; apply/esym/negP=>/andP [H1 H2]; elim: H. by apply/(rcons_lastXP _ y); rewrite H1 H2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)