proposition: Lemma consec_hd2 k1 k2 ks : uniq ks -> k1 \notin ks -> k2 \notin ks -> k1 != k2 -> consec [:: k1, k2 & ks] k1 k2.
proof: Proof. move=>U K1 K2 N; rewrite /consec !sltL eq_sym N /= nilp_hasPn. apply/hasPn=>z; apply: contraL=>/= _. rewrite eqslice_mem_uniq; last first. - by rewrite /= inE negb_or N K1 K2. rewrite negb_and; apply/orP; right. by rewrite in_itv /= (negbTE N) !eqxx /= negb_and ltEnat /= -!leqNgt leqn0 lt0n orbN. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)