proposition: Theorem MN_coeff_consE la m0 mu : MN_coeff la (m0 :: mu) = \sum_(sh : 'P_(sumn mu) | ribbon sh la) MN_coeff sh mu * (-1) ^+ (ribbon_height sh la).-1.
proof: Proof. apply esym; transitivity ( \sum_(sh <- enum_partn (sumn mu) | ribbon sh la) MN_coeff sh mu * (-1) ^+ (ribbon_height sh la).-1). by rewrite -enum_intpartnE [LHS]big_mkcond [RHS]big_mkcond big_map big_enum. rewrite big_mkcond /=; elim: enum_partn => [| p0 p] /=; first by rewrite big_nil. by rewrite big_cons => ->; case: (ribbon p0 la); rewrite //= add0r. 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