proposition: Lemma horner2_swapXY u x y : (swapXY u).[x, y] = u.[y, x].
proof: Proof. by rewrite horner_swapXY -{1}(hornerC y x) horner_map. 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)