proposition: Lemma consec_hdswap k1 k2 ks x : uniq ks -> k1 \notin ks -> k2 \notin ks -> x != k2 -> consec (k1::ks) k1 x -> consec (k2::ks) k2 x.
proof: Proof. move=>U K1 K2 N2 C. have N1 : x != k1 by move/consec_slt: C; rewrite sltL. move: C; rewrite /consec !sltL N1 N2 /= !nilp_hasPn. apply: contra=>/hasP [z Z] _; apply/hasP; exists z=>//. case/mem_oo: Z; first by rewrite /= K2. rewrite inE sltL slt_cons=>Z1 Nz /andP [_ Z2]. rewrite (negbTE Nz) /= in Z1 Z2. apply/mem_oo; first by rewrite /= K1. rewrite inE sltL slt_cons Z1 N1 Z2 /= orbT; split=>//. by apply: contra K1 => /eqP <-. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)