proposition: Lemma npolypK (p : {poly R}) : size p <= n -> npolyp p = p :> {poly R}.
proof: Proof. move=> spn; apply/polyP=> i; rewrite coef_npolyp. by have [i_big|i_small] // := ltnP; rewrite nth_default ?(leq_trans spn). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop binomial finset finfun ssralg countalg finalg poly polydiv) mathcomp(perm fingroup matrix mxalgebra mxpoly vector countalg)