proposition: Lemma poly_XaY0 : poly_XaY 0 = 0.
proof: Proof. by rewrite /poly_XaY rmorph0 comp_poly0. 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)