proposition: Lemma horner_swapXY u x : (swapXY u).[x%:P] = u ^ eval x.
proof: Proof. apply/polyP=> i /=; rewrite coef_map /= /eval horner_coef coef_sum -sizeYE. rewrite (horner_coef_wide _ (max_size_coefXY u i)); apply: eq_bigr=> j _. by rewrite -polyC_exp coefMC 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)