proposition: Lemma MN_coeff_rec_notincl la nu mu : 0%N \notin mu -> is_part nu -> ~~ included nu la -> MN_coeff_rec la nu mu = 0.
proof: Proof. elim: mu nu => [/= |[|m0] mu IHmu] nu //. by case: eqP => // ->; rewrite included_refl. rewrite inE negb_or eq_sym => /andP[_ {}/IHmu Hrec] partnu nincl. rewrite MN_coeff_rec_szE big_mkcond big_pmap /=; apply big1 => i _. case Haddrib : add_ribbon => [[sh h]|]//=. suff /negbTE -> : ~~ included sh la by []. by apply/contra : nincl => /(included_trans (included_add_ribbon partnu Haddrib)). 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