proposition: Lemma coef_swapXY u i j : (swapXY u)`_i`_j = u`_j`_i.
proof: Proof. elim/poly_ind: u => [|u p IHu] in i j *; first by rewrite raddf0 !coef0. rewrite raddfD !coefD /= swapXY_polyC coef_map /= !coefC coefMX. rewrite !(fun_if (fun q : {poly R} => q`_i)) coef0 -IHu; congr (_ + _). by rewrite unlock rmorphM /= map_polyX hornerMX coefMC coefMX. 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)