proposition: Lemma mult_symh_U k d i m : (('h_k : {mpoly R[n]}) * 'X_i ^+ d)@_m = ((mdeg m == (k + d)%N) && (m i >= d))%:R.
proof: Proof. Proof using. rewrite /symh_pol mulr_suml linear_sum /=; case: leqP => /= H. - pose Ud := (U_(i) *+ d)%MM. have Hleq : (Ud <= m)%MM. apply/mnm_lepP => j; rewrite mulmnE mnm1E. by case: eqP => /= [<- | _]; rewrite ?mul1n ?mul0n. rewrite andbT -(submK Hleq). case: (_ =P _) => [/eqP |Hdeg] /=. + rewrite mdegD mdegMn mdeg1 mul1n eqn_add2r => /eqP Hdeg. have Hbound : mdeg (m - Ud) < k.+1 by rewrite Hdeg. rewrite (bigD1 (BMultinom Hbound)) /=; last by rewrite Hdeg. rewrite mpolyXn -mpolyXD mcoeffX eq_refl /=. rewrite big1 ?addr0 // => m' /andP[_ ] Hneq. rewrite -mpolyXD mcoeffX. apply/boolRP; move: Hneq; apply contra. rewrite eqm_add2r => /eqP Heq. by apply/eqP/val_inj => /=. + rewrite big1 // => m' /eqP Hm'. rewrite mpolyXn -mpolyXD mcoeffX. apply/boolRP; apply/contra_notN: Hdeg => /eqP <-. by rewrite mdegD Hm' mdegMn mdeg1 mul1n. - rewrite andbF big1 // => m' _. rewrite mpolyXn -mpolyXD mcoeffX. apply/boolRP/eqP/mnmP => /(_ i). rewrite mnmDE mulmnE mnm1E eq_refl mul1n => Habs. by move: H; rewrite -Habs ltnNge leq_addl. 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