proposition: Lemma MN_coeff_rec_szE la nu m0 mu : MN_coeff_rec la nu (m0 :: mu) = \sum_(psh <- pmap (add_ribbon nu m0.-1) (iota 0 (size la)) | included psh.1 la) MN_coeff_rec la psh.1 mu * (-1) ^+ psh.2.-1.
proof: Proof. rewrite /=; elim: pmap => [|[sh0 h0] s IHs]/=; first by rewrite big_nil. by rewrite big_cons /= -{}IHs; case: included. 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