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