proposition: Lemma swapXY_is_multiplicative : multiplicative swapXY.
proof: Proof. split=> [u v|]; last by rewrite swapXY_polyC map_polyC. apply/polyP=> i; apply/polyP=> j; rewrite coef_swapXY !coefM !coef_sum. rewrite (eq_bigr _ (fun _ _ => coefM _ _ _)) exchange_big /=. apply: eq_bigr => j1 _; rewrite coefM; apply: eq_bigr=> i1 _. by rewrite !coef_swapXY. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice ssrnat seq) mathcomp(fintype tuple finfun bigop fingroup perm div) mathcomp(ssralg zmodp matrix mxalgebra) mathcomp(poly polydiv mxpoly binomial)