proposition: Lemma co_hpYE la (p q : pol) : map_mpoly (co_hp la) (p(X) * q(Y)) = (co_hp la q) *: p.
proof: Proof. rewrite polyXY_scale /=; apply/mpolyP => /= m. rewrite linearZ /= mcoeff_map_mpoly /= linearZ /= mulrC. rewrite /polX_XY /= mcoeff_map_mpoly /= mul_mpolyC. by rewrite mulrC -linearZ. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssrint rat ssralg ssrnum algC matrix vector) mathcomp(mpoly) tools partition ordtype antisym Schur_mpoly Schur_altdef sympoly homogsym permcent