proposition: Lemma npoly_enum_uniq : uniq npoly_enum.
proof: Proof. rewrite /npoly_enum; case: n=> [|k] //. rewrite pmap_sub_uniq // map_inj_uniq => [|f g eqfg]; rewrite ?enum_uniq //. apply/ffunP => /= i; have /(congr1 (fun p : {poly _} => p`_i)) := eqfg. by rewrite !coef_poly ltn_ord inord_val. 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)