proposition: Lemma card_npoly : #|{poly_n R}| = (#|R| ^ n)%N.
proof: Proof. rewrite cardE enumT unlock /= /npoly_enum; case: n => [|k] //=. rewrite size_pmap_sub (@eq_in_count _ _ predT) ?count_predT; last first. by move=> _ /mapP /= [f _ ->]; rewrite size_poly. by rewrite size_map -cardE card_ffun card_ord. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop binomial finset finfun zmodp ssralg countalg finalg poly polydiv) mathcomp(perm fingroup) CoqEAL(hrel pos param refinements binnat boolF2 seqpoly poly_op trivial_seq poly_div boolF2)