proposition: Lemma card_npoly : #|{poly_n R}| = (#|R| ^ n)%N.
proof: Proof. rewrite -(card_imset _ (can_inj (@npoly_rV_K _ _))) eq_cardT. by rewrite -cardT /= card_mx mul1n. by move=> v; apply/imsetP; exists (rVnpoly v); rewrite ?rVnpolyK //. 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)