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