proposition: Lemma size_norm_poly2 p : size (norm_poly2 p) = size p.
proof: Proof. rewrite /norm_poly2; have [->|p0] := eqVneq p 0. by rewrite /map_poly poly_def !(size_poly0, big_ord0). rewrite /map_poly size_poly_eq // -size_poly_eq0 size_poly_eq //. by rewrite -lead_coefE size_poly_eq0 lead_coef_eq0. by rewrite -!lead_coefE normr_eq0 !lead_coef_eq0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial bigenough)