proposition: Lemma mem_npoly_enum p : p \in npoly_enum.
proof: Proof. rewrite /npoly_enum; case: n => [|k] // in p *. by case: p => [p sp] /=; rewrite in_cons -val_eqE /= -size_poly_leq0 sp. rewrite mem_pmap_sub; apply/mapP. eexists [ffun i : 'I__ => p`_i]; first by rewrite mem_enum. apply/polyP => i; rewrite coef_poly. have [i_small|i_big] := ltnP; first by rewrite ffunE /= inordK. by rewrite nth_default // 1?(leq_trans _ i_big) // size_npoly. 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)