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