proposition: Lemma uniq_uo_filter s i : uniq s -> &=s `]-oo, i[ = [seq x <- s | x <[s] i].
proof: Proof. move=>U; rewrite /eq_slice /= /slice /= drop0 addn0. elim: s U=>//=h s IH. case/andP=>Nh U; rewrite slt_cons eqxx /= andbT. case: (eqVneq i h)=>[E|N] /=. - rewrite -{h}E in Nh *; rewrite -(filter_pred0 s). by apply: eq_in_filter=>z Hz /=; rewrite slt_cons eqxx. congr (cons _); rewrite IH //; apply: eq_in_filter=>z Hz. rewrite slt_cons N /=. suff: (z != h) by move/negbTE=>->. by apply: contraNneq Nh=><-. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)