proposition: Lemma consec_next (ks : seq A) x y z : uniq ks -> consec ks x y -> x <[ks] z -> y <=[ks] z.
proof: Proof. move=>U; case/(consecP_ingt _ _ U)=>X E N; case Dz : (z \in ks); first by rewrite E. by apply: sle_memI; rewrite Dz. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)