proposition: Lemma alt_homog : 'a_(rho) \is 'C(n, 2).-homog.
proof: Proof. Proof using. apply rpred_sum => s _; rewrite rpredZsign msymX dhomogX /=. have -> : mdeg (rho#(s^-1)%g) = mdeg rho. by rewrite /mdeg; apply/perm_big/tuple_permP; exists (s^-1)%g. by rewrite mdeg_rho. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition