proposition: Lemma mem_enum_permuted (s t : n.-tuple T) : perm_eq s t -> t \in permuted_tuple s.
proof: Proof. Proof using. rewrite perm_sym => /tuple_permP[perm Hperm]. apply/mapP; exists perm; first by rewrite mem_enum. by apply val_inj; rewrite /= Hperm. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup action gproduct) tools combclass sorted partition composition multinomial permcomp cycles