proposition: Lemma hasNL_xx (ks : seq A) t1 t2 (p : pred A) : uniq ks -> t1 <=[ks] t2 -> ~~ has p (&=ks `[t1, t2]) -> {in ks, forall z, p z -> z <=[ks] t2 = z <[ks] t1}.
proof: Proof. move=>U T /hasPn H z K P. move: (H z); rewrite eqslice_mem_uniq // in_itv K /= =>/contraL/(_ P). rewrite negb_and -!sltNge; case/orP=>Hz. - by rewrite Hz; apply/sltW/(slt_sle_trans Hz). rewrite sltNge sleNgt Hz; congr negb; apply/esym. by apply/sltW/(sle_slt_trans T). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)