proposition: Lemma uniq_take i (s : seq A) : i < size s -> uniq s -> uniq (take i s).
proof: Proof. elim: i s => [l _ _ |i IH [| h t] //=]; first by rewrite take0. rewrite ltnS => nt /andP[ht ut]. rewrite (IH _ nt ut) andbT; apply: contra ht; exact: mem_take. Qed.
imports: mathcomp(all_ssreflect fingroup perm)