proposition: Lemma slice_uniq s i : uniq s -> uniq (&:s i).
proof: Proof. move=>U; rewrite /slice /=; case: i=>l u. by apply/drop_uniq/take_uniq. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)