proposition: Lemma consec_prevX (ks : seq nat) x : uniq ks -> x \in ks -> ks = x :: behead ks \/ exists y, consec ks y x.
proof: Proof. case: (not_memX ks)=>k N U X. have U' : uniq (k :: ks) by rewrite /= N U. have : k <[k::ks] x by rewrite sltL; case: eqP X N=>// ->->. case/(olt_consec_prev _ _ U')=>t [_]; rewrite consec_consEP' //. by case: eqP X=>[_ ->|_ _ []]; [left|right; exists t]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)