proposition: Lemma swapXY_comp_poly p u : swapXY (p^:P \Po u) = p^:P \Po swapXY u.
proof: Proof. rewrite -horner_map; congr _.[_]; rewrite -!map_poly_comp /=. by apply: eq_map_poly => x; rewrite /= swapXY_polyC map_polyC. 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)