proposition: Lemma hasNL_oo (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 -!sleNgt; case/orP=>Hz. - by rewrite Hz; apply: (sle_slt_trans Hz). rewrite sltNge Hz sleNgt; congr negb; apply/esym. by apply: (slt_sle_trans T). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)