proposition: Lemma swapXY_poly_XmY p : swapXY (poly_XmY p) = poly_XmY p.
proof: Proof. by rewrite swapXY_comp_poly rmorphM /= swapXY_X swapXY_Y commr_polyX. 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)