proposition: Lemma has_uo t (ks : seq A) : uniq ks -> has predT (&=ks `]-oo, t[) = has (fun z => z <[ks] t) 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)