proposition: Lemma mem_split_uniq (x : A) s : x \in s -> uniq s -> exists s1 s2, [/\ s = s1 ++ [:: x] ++ s2, uniq (s1 ++ s2) & x \notin s1 ++ s2].
proof: Proof. move=>/[swap] Hu /mem_split [s1 [s2 H]]. exists s1, s2; move: Hu. by rewrite H uniq_catCA cons_uniq; case/andP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq eqtype path fintype finfun tuple interval perm fingroup) pcm(options prelude ordtype seqext slice)