proposition: Lemma cnvar_prodgen d (la : 'P_d) : (d <= m) || (n <= m) -> cnvarsym (prod_gen (Gen m) la) = prod_gen (Gen n) la.
proof: Proof. move=> Hd; rewrite /prod_gen rmorph_prod. apply eq_big_seq => i Hin. have := intpartn_leq Hin. move: Hin => /(in_part_non0 (intpartnP la)). case: i => //= i _ Hi; apply Hcnvargen. move: Hd => /orP[Hd | ->]; last by rewrite orbT. by apply/orP; left; apply: (leq_trans Hi Hd). 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