proposition: Lemma MN_coeff_rec_consE n la nu m0 mu : m0 != 0%N -> size la <= n -> MN_coeff_rec la nu (m0 :: mu) = \sum_(psh <- pmap (add_ribbon nu m0.-1) (iota 0 n) | included psh.1 la) MN_coeff_rec la psh.1 mu * (-1) ^+ psh.2.-1.
proof: Proof. case: m0 => // m0 _ Hsz; rewrite MN_coeff_rec_szE. rewrite big_mkcond big_pmap -(subn0 (size la)) -/(index_iota 0 _) /=. rewrite [RHS]big_mkcond big_pmap -(subn0 n) -/(index_iota 0 _) /=. rewrite (big_cat_nat _ _ _ _ Hsz) //=. rewrite [X in _ + X]big_nat [X in _ + X]big1 ?addr0 // => i /andP[leszi _]. case Haddrib : add_ribbon => [[sh h]|]//=. suff /negbTE -> : ~~ included sh la by []. apply/negP => /includedP[+ _]. by rewrite (size_add_ribbon Haddrib) geq_max ltnNge leszi andbF. 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