proposition: Lemma consec_nextX (ks : seq nat) x : uniq ks -> x \in ks -> (exists ks', ks = rcons ks' x) \/ exists y, consec ks x y.
proof: Proof. case: (not_memX ks)=>k N U X. have Ur : uniq (rcons ks k) by rewrite rcons_uniq N U. have : x <[rcons ks k] k by rewrite slt_rcons (negbTE N) eq_refl orbF. case/(olt_consec_next _ _ Ur)=>t []. rewrite consec_rconsEP' //. case: eqP X N=>[->->//|/eqP Nkx X N /=]. case T: (t \in ks)=>/=; first by right; exists t. by case=>-> {t T} [ks' -> _]; left; exists ks'. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)