proposition: Lemma hasNL_ux (ks : seq A) t (p : pred A) : uniq ks -> ~~ has p (&=ks `]-oo, t]) -> {in ks, forall z, p z -> t <[ks] z}.
proof: Proof. move=>U /hasPn H z K P. move: (H z); rewrite eqslice_mem_uniq // in_itv K /= =>/contraL/(_ P). by rewrite -sltNge. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)