proposition: Lemma syms_prod_sympM_int dn (nu : 'P_dn) dm (mu : 'P_dm) : 's[nu] * 'p[mu] = \sum_(la : 'P_(dn + dm)) MN_coeff_rec la nu mu *: 's[la] :> {sympoly int[n]}.
proof: Proof. case: mu => [mu /= Hnu]; rewrite /prod_symp /prod_gen /=. move: Hnu => /andP[/eqP <-{dm} /notin0_part]. elim: mu dn nu => [|m0 mu IHmu] d nu. rewrite big_nil mulr1 (bigD1 (cast_intpartn (esym (addn0 d)) nu)) //=. rewrite syms_cast cast_intpartnE // eqxx scale1r. rewrite big1 ?addr0 // => la. rewrite -val_eqE /= cast_intpartnE => /negbTE ->. by rewrite scale0r. rewrite inE negb_or eq_sym => /andP[Hm0 Hmu]. rewrite big_cons mulrA syms_sympM_oapp //. move Hmmu : (m0 :: mu) => mmu. rewrite [RHS](bigID (fun sh => size (val sh) <= n)) /=. rewrite [X in _ + X]big1 ?addr0; first last => [la|]. by rewrite -ltnNge => /syms_oversize ->; rewrite scaler0. under [RHS]eq_bigr => la Hla. rewrite -{2}Hmmu (MN_coeff_rec_consE _ _ Hm0 Hla). rewrite big_mkcond big_pmap. rewrite -[n in iota 0 n](subn0 n) -/(index_iota 0 n) big_mkord /=. by rewrite scaler_suml over. rewrite [RHS]exchange_big /= mulr_suml; apply: eq_bigr => i _. rewrite -{mmu}Hmmu; case: m0 Hm0 => // m0 _ /=. rewrite add_ribbon_intpartnE. case Haddrib: add_ribbon_intpartn => [[res h]|]/=; first last. by rewrite mul0r; apply/esym/big1 => t; rewrite scale0r. rewrite -scalerAl {}IHmu // scaler_sumr. have cast_eq : (d + (m0.+1 + sumn mu) = m0.+1 + d + sumn mu)%N. by rewrite [(m0.+1 + d)%N]addnC addnA. rewrite (reindex _ (onW_bij _ (cast_intpartn_bij cast_eq))) /=. under [LHS]eq_bigr do rewrite cast_intpartnE syms_cast /=. rewrite [LHS](bigID (fun sh => size (val sh) <= n)) /=. rewrite [X in _ + X]big1 ?addr0; first last => [la|]. by rewrite -ltnNge => /syms_oversize ->; rewrite !scaler0. apply eq_bigr => la szla. case: (boolP (included res la)) => incl; first by rewrite scalerA mulrC. by rewrite MN_coeff_rec_notincl // !scale0r scaler0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint perm fingroup tuple vector rat) mathcomp(ssrcomplements freeg mpoly monalg) sorted tools ordtype permuted partition skewpart antisym Schur_mpoly Schur_altdef sympoly homogsym