proposition: Lemma poly_XmY_eq0 p : (poly_XmY p == 0) = (p == 0).
proof: Proof. by rewrite -!size_poly_eq0 size_poly_XmY. 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)