proposition: Lemma consec_cons k ks x y : uniq ks -> k \notin ks -> x != k -> y != k -> consec ks x y -> consec (k::ks) x y.
proof: Proof. move=>U N Nx Ny; rewrite /consec slt_cons Ny (negbTE Nx) /=. case/andP=>->/=; rewrite !nilp_hasPn; apply: contra. case/hasP=>z Z _; apply/hasP; exists z=>//. case/mem_oo: Z; first by rewrite /= N. rewrite inE !slt_cons (negbTE Nx) Ny !(eq_sym z) /=. case: eqVneq=>//= _ Hz Hxz Hzy. by apply/mem_oo. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)