proposition: Lemma symp_to_symm k : 'p_k.+1 = 'm[rowpartn k.+1] :> SP.
proof: Proof. case: n => [|n0]. apply/val_inj; rewrite [RHS]nvar0_mpolyC [LHS]nvar0_mpolyC. rewrite (dhomog_nemf_coeff (symm_homog 0 R (rowpartn k.+1))); last by rewrite /= mdeg0. by rewrite (dhomog_nemf_coeff (symp_homog 0 R k.+1)) //= mdeg0. move HK : k.+1 => K. rewrite (homog_symmE (symp_homog n0.+1 R K)) (bigD1 (rowpartn K)) //=. have -> : (symp_pol n0.+1 R K)@_(mpart (rowpartn K)) = 1. rewrite /symp_pol (bigD1 ord0) // raddfD raddf_sum //. rewrite mpolyXn [rowpartn _]lock /= mcoeffX -HK. rewrite -{1}lock expUmpartNE /= eqxx big1 ?addr0 // => i /negbTE Hi. by rewrite mpolyXn /= mcoeffX expUmpartNE Hi. rewrite scale1r big1 ?addr0 -{}HK // => P /negbTE HP. suff -> : (symp_pol n0.+1 R k.+1)@_(mpart P) = 0 by rewrite scale0r. rewrite /symp_pol raddf_sum big1 ?mcoeff0 //= => i _. by rewrite mpolyXn /= mcoeffX expUmpartNE HP andbF. 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