proposition: Lemma has_ox t1 t2 (ks : seq A) : uniq ks -> has predT (&=ks `]t1, t2]) = has (fun z => t1 <[ks] z && z <=[ks] t2) ks.
proof: Proof. by move/has_predT_uslice=>->; apply: eq_has=>z; rewrite in_itv. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)