proposition: Lemma rho_uniq : uniq rho.
proof: Proof. Proof using . suff : perm_eq rho (iota 0 n) by move/perm_uniq ->; exact: iota_uniq. by rewrite rho_iota perm_sym -perm_rev. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition