proposition: Lemma mult_syme_U k d i m : (('e_k : {mpoly R[n]}) * 'X_i ^+ d)@_m = [&& mdeg m == (k + d)%N, (d <= m i <= d.+1) & [forall j : 'I_n, (j != i) ==> (m j <= 1%N)]]%:R.
proof: Proof. Proof using. rewrite mpolyXn. case: (_ =P _) => /= [degm | /eqP/negbTE Hneq]; first last. have /dhomog_nemf_coeff -> // : (('e_k : {mpoly R[n]}) * 'X_[(U_( i) *+ d)]) \is (k + d).-homog. by rewrite dhomogM ?syme_homog // dhomogX /= mdegMn mdeg1 mul1n. by rewrite /= Hneq. case: leqP => /= dmi; first last. apply/memN_msupp_eq0/negP. rewrite (perm_mem (msuppMX _ _)) => /mapP[/=[mon _]]. move=> /(congr1 (fun m => m i)) Hmi; move: dmi; rewrite {}Hmi. by rewrite mnmDE mulmnE mnmE eqxx mul1n leqNgt ltnS leq_addr. case: leqP => /= dmi2; first last. apply/memN_msupp_eq0/negP. rewrite (perm_mem (msuppMX _ _)) => /mapP[/=[mon]]. rewrite mem_msupp_mesym /mechar => /andP[_ /forallP /= /(_ i) Hmon]. move=> /(congr1 (fun m => m i)) Hmi; move: dmi2; rewrite {}Hmi. rewrite mnmDE mulmnE mnmE eqxx mul1n. by rewrite leqNgt !(addSn, ltnS) -(addn1 d) leq_add2l Hmon. case: (boolP [forall _, _]) => [/forallP Hall | /=]; first last. rewrite negb_forall => /existsP[/= j]. rewrite negb_imply -ltnNge => /andP[/negbTE neji mj]. apply/memN_msupp_eq0/negP. rewrite (perm_mem (msuppMX _ _)) => /mapP[/=[mon]]. rewrite mem_msupp_mesym /mechar => /andP[_ /forallP /= /(_ j) Hmon]. move=> /(congr1 (fun m => m j)) Hmj; move: mj; rewrite {}Hmj. by rewrite mnmDE mulmnE mnmE eq_sym {}neji mul0n add0n leqNgt ltnS Hmon. have {}Hall x : x != i -> m x <= 1 by move=> H; apply: (implyP (Hall x)). have leqUm : (U_(i) *+ d <= m)%MM. apply/mnm_lepP => j; rewrite mulmnE mnmE. by case: eqP => [<-|]; rewrite ?muln0 // mul1n. rewrite -(submK leqUm) addmC mcoeffMX mcoeff_mesym /mechar. move: leqUm => /submK/(congr1 mdeg); rewrite mdegD degm mdegMn mdeg1 mul1n. move/eqP; rewrite eqn_add2r => /eqP ->; rewrite eqxx /=. case: forallP => // H; exfalso; apply: H => /= j. rewrite mnmBE mulmnE mnmE eq_sym. case: (_ =P _) => [->{j} | /eqP/Hall]; last by rewrite mul0n subn0. by rewrite mul1n leq_subLR addn1. 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