proposition: Lemma mult_altern_symp_pol p d : 'a_(mpart p + rho) * (symp_pol n R d.+1) = \sum_(i < n) 'a_(mpart p + rho + U_(i) *+ d.+1).
proof: Proof. rewrite /alternpol mulr_suml [RHS]exchange_big /=; apply eq_bigr => s _. rewrite -scaler_sumr -scalerAl; congr (_ *: _). rewrite -(issymP _ (symp_sym n R d.+1) s) -msymM -linear_sum /=; congr msym. rewrite /symp_pol mulr_sumr; apply eq_bigr => i _. by rewrite !mpolyXD mpolyXn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint perm fingroup tuple vector rat) mathcomp(ssrcomplements freeg mpoly monalg) sorted tools ordtype permuted partition skewpart antisym Schur_mpoly Schur_altdef sympoly homogsym