proposition: Lemma mdeg_rho : mdeg rho = 'C(n, 2).
proof: Proof. rewrite /mdeg binomial_sumn_iota sumnE. by apply: perm_big; 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