proposition: Lemma symh0 : 'h_0 = 1.
proof: Proof. Proof using. have Hd0 : (mdeg (0%MM : 'X_{1..n})) < 1 by rewrite mdeg0. apply val_inj => /=. rewrite /symh_pol /symh_pol_bound (big_pred1 (BMultinom Hd0)); first last. by move=> m; rewrite /= mdeg_eq0 {2}/eq_op. by rewrite mpolyX0. 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