proposition: Lemma nseq_cat l l' n : l ++ l' = nseq n a -> l' = nseq (n - size l) a.
proof: Proof. move=> ll'na; move/(congr1 (drop (size l))) : (ll'na). rewrite drop_cat ltnn subnn drop0 => ->. move: (nseq_add (size l) a (n - size l)). rewrite subnKC; last by rewrite -(size_nseq n a) -ll'na size_cat leq_addr. by move=> ->; rewrite drop_cat size_nseq ltnn subnn drop0. Qed.
imports: mathcomp(all_ssreflect fingroup perm)