proposition: Lemma consec_nextN (ks : seq A) x y z : uniq ks -> y \in ks \/ z \in ks -> y != z -> consec ks x y -> x <[ks] z -> y <[ks] z.
proof: Proof. move=>U /orP D N C /(consec_next U C). by rewrite (sle_eqVlt D) (negbTE N). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)