proposition: Lemma npolyX_coords (p : {poly_n K}) i : coord npolyX i p = p`_i.
proof: Proof. rewrite [p in RHS](coord_basis npolyX_full) ?memvf // coefn_sum. rewrite (bigD1 i) //= coefZ nth_npolyX npolyXE coefXn eqxx mulr1 big1 ?addr0//. move=> j; rewrite -val_eqE => /= neq_ji. by rewrite coefZ nth_npolyX npolyXE 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)