proposition: Lemma uniq_ux_filter s i : uniq s -> &=s `]-oo, i] = [seq x <- s | x <=[s] i].
proof: Proof. move=>U; rewrite /eq_slice /= /slice /= drop0 addn1. elim: s U=>//=h s IH. case/andP=>Nh U; rewrite sle_cons eqxx /=. congr (cons _); case: (eqVneq i h)=>[E|N]. - rewrite -{h}E in Nh *; rewrite take0 -(filter_pred0 s). apply: eq_in_filter=>z Hz /=; rewrite sle_cons eqxx /= orbF. by apply/esym/negbTE; apply: contraNneq Nh=><-. rewrite IH //; apply: eq_in_filter=>z Hz; rewrite sle_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)