proposition: Lemma permutedP (p : permuted) : perm_eq w p.
proof: Proof. Proof using. by case: p. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup action gproduct) tools combclass sorted partition composition multinomial permcomp cycles