proposition: Lemma mcoeff_symh_pol_bound b d m : b > d -> (symh_pol_bound b d)@_m = (mdeg m == d)%:R.
proof: Proof. rewrite linear_sum /= => H. case: (mdeg m =P d) => Hd /=. - have Hsm : mdeg m < b by rewrite Hd. rewrite (bigD1 (BMultinom Hsm)) ?Hd //= mcoeffX eq_refl big1 ?addr0 //=. by move=> mon /andP[_ /negbTE]; rewrite {1}/eq_op /= mcoeffX => ->. - rewrite big1 // => mon /eqP Hd1; rewrite mcoeffX. by apply/boolRP; move: Hd; rewrite -{1}Hd1; apply contra_notN => /eqP ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(ssrcomplements freeg mpoly) sorted tools ordtype permuted partition skewpart composition Yamanouchi std tableau stdtab skewtab permcent antisym Schur_mpoly therule Schur_altdef unitriginv