proposition: Lemma mul_ek_p1 (k : nat) : 'e_k.+1 * 'p_1 = k.+2%:R *: 'e_k.+2 + 'm[hookpartn k.+2 1] :> SF.
proof: Proof. case: (leqP k.+1 n) => [ltkn | Hkn]; first last. rewrite !syme_geqnE //; last exact: ltnW. by rewrite mul0r scaler0 add0r symm_oversize // size_hookpartn. have /homog_symmE -> : sympol ('e_k.+1 * 'p_1: SF) \is k.+2.-homog. by rewrite -(addn1 k.+1) dhomogM ?syme_homog ?symp_homog. rewrite (syme_to_symm _ _ k.+2). rewrite (bigD1 (hookpartn k.+2 1)) //=/symp_pol {1}mulr_sumr !raddf_sum /=. rewrite [RHS]addrC -[X in _ = X + _]scale1r; congr ((_ *: _) + _). have szhk11 : size (hookpartn k.+2 1) = k.+1 by rewrite size_hookpartn. rewrite (bigD1 ord0) //= big1 ?addr0; first last. case: (n =P 1%N) => [neq1 [i Hi] | /eqP nneq1 i /negbTE in0]. by rewrite -val_eqE /= -lt0n leqNgt -neq1 Hi. rewrite mult_syme_U. case: (boolP [&& _, _ & _]) => // /and3P[_ _ /forallP/(_ ord0)]. rewrite eq_sym {}in0 /= /mpart szhk11 ltkn. by rewrite mnmE hookpartnE. rewrite mult_syme_U. rewrite mdeg_mpart ?szhk11 // sumn_intpartn addn1 eqxx /=. rewrite {1 2}/mpart szhk11 ltkn mnmE {1 2}hookpartnE //=. case: forallP => // H; exfalso; apply: H => /= j. apply/implyP => /negbTE jn0. rewrite /mpart szhk11 ltkn mnmE hookpartnE /= //. case: j jn0 => [[|j]] //= Hj _ {Hj}. by rewrite nth_nseq; case: ltnP. rewrite (bigD1 (colpartn k.+2)) /=; first last. by rewrite -val_eqE /= colpartnE !hookpartnE. rewrite [X in _ + X]big1 ?addr0 => [| la /andP[lahk lacol] ]; first last. case: (leqP (size la) n) => szla; last by rewrite symm_oversize // scaler0. rewrite {1}mulr_sumr !raddf_sum /= big1 ?scale0r // => i /= _. rewrite mult_syme_U. case: (boolP [&& _, _ & _]) => //= /and3P[_ H2 /forallP H]; exfalso. case: (i =P ord0) => [ieq0 | /eqP ineq0]. - subst i; case Hla0 : (mpart la ord0) H2 => [|[|[|l0]]] _ //=. + move: Hla0 {lahk H}; rewrite /mpart {}szla mnmE //= => la0. move: lacol; rewrite (colpartnP (x0 := 0) (la := la)) ?eqxx //. by rewrite -nth0; case: la la0 => [[|l0 la]] //= _ ->. + move: Hla0 {lacol}; rewrite /mpart szla mnmE //= => la0. move: lahk; suff -> : la = hookpartn k.+2 1 by rewrite eqxx. case: (ltnP 1 n) => [lt1n|]; first last. rewrite ltnS leqn0 => /eqP Hn; subst n0. move: ltkn; rewrite ltnS leqn0 => /eqP Hk; subst k. rewrite hookpartn_row; case: (intpartn2 la) => [-> // | lacol]. by move: szla; rewrite lacol size_colpartn. move/(_ (Ordinal lt1n)): H; rewrite -val_eqE /=. rewrite /mpart szla /= mnmE /= => /(hookpartnPE 0) ->. by rewrite la0. - move: (H ord0) lacol; rewrite eq_sym {}ineq0 /= /mpart szla mnmE. by move/colpartnP => ->; rewrite eqxx. case: (leqP k.+2 n) => {ltkn}ltk1n; first last. by rewrite !symm_oversize ?size_colpartn // !scaler0. congr (_ *: _); rewrite mulr_sumr raddf_sum /=. rewrite (bigID (fun i : 'I_n => i < k.+2)) /=. rewrite [X in _ + X]big1 ?addr0 => [|i]; first last. rewrite -leqNgt mult_syme_U => ltk1i. case: (boolP [&& _, _ & _]) => //= /and3P[_ Hnthi _]; exfalso. move: Hnthi; rewrite /mpart size_colpartn ltk1n mnmE colpartnE nth_nseq. by rewrite (ltnNge i _) ltk1i. transitivity (\sum_(0 <= i < k.+2) 1 : R); last by rewrite sumr_const_nat subn0. rewrite [RHS](big_nat_widen _ _ _ _ _ ltk1n) big_mkord /=. apply eq_bigr => i ltik2. rewrite mult_syme_U. rewrite mdeg_mpart ?size_colpartn // sumn_intpartn addn1 eqxx /=. rewrite /mpart size_colpartn ltk1n mnmE {1 2}colpartnE nth_nseq ltik2 /=. case: forallP => // H; exfalso; apply: H => /= j. apply/implyP => /negbTE jn0. by rewrite mnmE colpartnE nth_nseq; case: ltnP. 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