proposition: Lemma horner_poly_XaY p v : (poly_XaY p).[v] = p \Po (v + 'X).
proof: Proof. by rewrite horner_comp !hornerE. 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)