proposition: Lemma mul_ek_pk (k l : nat) : 'e_k.+1 * 'p_l.+2 = 'm[hookpartn (k + l).+3 l.+1] + 'm[hookpartn (k + l).+3 l.+2] :> SF.
proof: Proof. have szhook2 : size (hookpartn (k + l).+3 l.+2) = k.+1. rewrite size_hookpartn; last by rewrite !ltnS leq_addl. by rewrite !subSS -!addSn addnK. have szhook1 : size (hookpartn (k + l).+3 l.+1) = k.+2. rewrite size_hookpartn; last by rewrite !ltnS -addSn leq_addl. by rewrite !subSS -!addSn addnK. have hook2ok : l.+1 < (k + l).+2 by rewrite !ltnS leq_addl. have hook1ok : l < (k + l).+2 by apply ltnW. case: (leqP k.+1 n) => [ltkn | Hkn]; first last. rewrite !syme_geqnE // mul0r. by rewrite !symm_oversize ?addr0 // ?szhook1 ?szhook2 //; apply ltnW. have /homog_symmE -> : sympol ('e_k.+1 * 'p_l.+2: SF) \is (k + l).+3.-homog. by rewrite -addSn -!addnS dhomogM ?syme_homog ?symp_homog. rewrite (bigD1 (hookpartn (k + l).+3 l.+2)) //=. rewrite /symp_pol {1}mulr_sumr !raddf_sum /=. rewrite [RHS]addrC -[X in _ = X + _]scale1r; congr ((_ *: _) + _). rewrite {szhook1 hook1ok} (bigD1 ord0) //= big1 ?addr0; first last. case: (n =P 1%N) => [neq1 [i ltin]| _ i /negbTE in0]. by rewrite -val_eqE /= -lt0n leqNgt -neq1 ltin. rewrite mult_syme_U. case: (boolP [&& _, _ & _]) => // /and3P[_ _ /forallP/(_ ord0)]. rewrite eq_sym {}in0 /= /mpart szhook2 ltkn. by rewrite mnmE hookpartnE. rewrite mult_syme_U. rewrite mdeg_mpart ?szhook2 // sumn_intpartn !addSn !addnS eqxx /=. rewrite {1 2}/mpart szhook2 ltkn mnmE. rewrite {1 2}hookpartnE //= leqnSn leqnn /=. case: forallP => // H; exfalso; apply: H => /= j. apply/implyP => /negbTE jn0. rewrite /mpart szhook2 ltkn mnmE hookpartnE //=. case: j jn0 => [[|j]]//= Hj _ {Hj}. by rewrite nth_nseq; case: ltnP. rewrite (bigD1 (hookpartn (k + l).+3 l.+1)) //=; first last. by rewrite -val_eqE /= !hookpartnE //= eqseq_cons !eqSS presentSn.ieqi1F. rewrite /symp_pol {1}mulr_sumr !raddf_sum /=. rewrite -[RHS]addr0; congr (_ + _). case: (leqP k.+2 n) => {ltkn} ltk1n; first last. by rewrite !symm_oversize ?size_colpartn ?szhook1 // !scaler0. rewrite {szhook2 hook2ok} (bigD1 ord0) //= big1 ?addr0; first last. case: (n =P 1%N) => [ltin [i ine0]| _ i /negbTE ine0]. by rewrite -val_eqE /= -lt0n leqNgt -ltin ine0. rewrite mult_syme_U. case: (boolP [&& _, _ & _]) => // /and3P[_ _ /forallP/(_ ord0)]. rewrite eq_sym {}ine0 /= /mpart szhook1 ltk1n. by rewrite mnmE hookpartnE. rewrite -[RHS]scale1r; congr (_ *: _). rewrite mult_syme_U. rewrite mdeg_mpart ?szhook1 // sumn_intpartn !addSn !addnS eqxx /=. rewrite {1 2}/mpart szhook1 ltk1n mnmE. rewrite {1 2}hookpartnE //= leqnSn leqnn /=. case: forallP => // H; exfalso; apply: H => /= j. apply/implyP => /negbTE jn0. rewrite /mpart szhook1 ltk1n mnmE hookpartnE //=. case: j jn0 => [[|j]]//= Hj _ {Hj}. by rewrite nth_nseq; case: ltnP. rewrite {szhook1 hook1ok szhook2 hook2ok} big1 => [| la /andP[lahk1 lahk2]]//. 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[_ Hnthi /forallP H]; exfalso. case: (ltnP 1 n) => [lt1n|neq1]; first last. have {}neq1 : n = 1%N. by apply anti_leq; rewrite neq1 /= (leq_ltn_trans _ ltkn). move: ltkn {lahk2 H}; rewrite neq1 ltnS leqn0 => /eqP Hk; subst k. move: szla; rewrite {}neq1. case: la Hnthi lahk1 => [[|l0 [|]]] //= H _. rewrite -val_eqE /= add0n hookpartn_row rowpartnE. move: H; rewrite addn0 add0n => /andP[/eqP ->]. by rewrite eqxx. case: (i =P ord0) => [ieq0 | /eqP/negbTE ineq0]. - subst i; move: Hnthi; rewrite /mpart szla mnmE => /andP/= [H1 H2]. move: lahk1 lahk2. move/(_ (Ordinal lt1n)): H; rewrite -val_eqE /=. rewrite /mpart szla /= mnmE /= => /(hookpartnPE 0). case (leqP (nth 0%N la 0) l.+2) => H3. + have {H1 H2 H3} -> /= : nth 0%N la 0 = l.+2. by apply/esym/anti_leq; rewrite H1 H3. by move=> ->; rewrite eqxx. + have {H1 H2 H3} -> /= : nth 0%N la 0 = l.+3. by apply/esym/anti_leq; rewrite H3 H2. by move=> ->; rewrite eqxx. - move: (H ord0) Hnthi; rewrite eq_sym {lahk1 lahk2}ineq0 /= /mpart szla mnmE. move/colpartnP ->; rewrite mnmE /= colpartnE nth_nseq. by case: (i < _). 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