proposition: Lemma consec_behead k ks x y : uniq ks -> k \notin ks -> x != k -> consec (k::ks) x y -> y != k /\ consec ks x y.
proof: Proof. by move=>U K Nx /(consec_consEP _ _ U K); rewrite (negbTE Nx). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)