proposition: Lemma prod_prodgen : (forall d, 'gA_d = \sum_(la : 'P_d) co la *: 'gB[la] :> SF) -> forall d (la : 'P_d), 'gA[la] = \sum_(mu : 'P_d) coeff_prodgen la mu *: 'gB[mu] :> SF.
proof: Proof. rewrite /coeff_prodgen /= {2}/prod_gen => H d la. have := sumn_intpartn la. case: la => [la /= Hla] Hd; subst d. under [RHS]eq_bigr do rewrite coeff_prodgen_cast //. elim: la {Hla} => [| l la IHla] /=. rewrite big_nil (big_pred1 (rowpartn 0)) ?prod_gen0 ?scale1r // => la. by symmetry; apply/eqP/val_inj; rewrite /= intpartn0. rewrite big_cons H; symmetry. under [LHS]eq_bigr do rewrite scaler_suml. rewrite (exchange_big_dep xpredT) //=. under [LHS]eq_bigr do rewrite big_pred1_eq -prod_genM -scalerA scalerAr scalerAl. rewrite -[LHS](pair_big xpredT xpredT (fun mu nu => _ mu *: _ mu * (_ nu *: _ nu))) /=. rewrite mulr_suml. by under eq_bigr do rewrite -mulr_sumr -IHla. 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