proposition: Lemma swapXY_is_scalable : scalable_for (map_poly polyC \; *%R) swapXY.
proof: Proof. by move=> p u /=; rewrite -mul_polyC rmorphM /= swapXY_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)