proposition: Lemma eq_seqE s s1 : perm_eq s s1 -> s1 \in permuted_seq s.
proof: Proof. Proof using. exact: perm_eq_permuted_tuple. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup action gproduct) tools combclass sorted partition composition multinomial permcomp cycles