proposition: Lemma mult_altern_pmap p d : is_part p -> size p <= n -> 'a_(mpart p + rho) * (symp_pol n R d.+1) = \sum_(psh <- pmap (add_ribbon p d) (iota 0 n)) (-1) ^+ (psh.2).-1 *: 'a_(mpart psh.1 + rho).
proof: Proof. move=> partp szp; rewrite mult_altern_oapp //. rewrite -(big_mkord xpredT (fun i => oapp _ 0 (add_ribbon p d i))). by rewrite big_pmap /index_iota subn0. 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