proposition: Lemma npolyX_free : free npolyX.
proof: Proof. apply/freeP=> u /= sum_uX_eq0 i; have /npolyP /(_ i) := sum_uX_eq0. rewrite (@big_morph _ _ _ 0%R +%R) // coef_sum coef0. rewrite (bigD1 i) ?big1 /= ?addr0 ?coefZ ?(nth_map 0%N) ?size_iota //. by rewrite nth_npolyX npolyXE coefXn eqxx mulr1. move=> j; rewrite -val_eqE /= => neq_ji. by rewrite nth_npolyX npolyXE coefZ coefXn eq_sym (negPf neq_ji) mulr0. 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)