proposition: Lemma coef_map_id0 p i : f 0 = 0 -> (p^f)`_i = f p`_i.
proof: Proof. by move=> f0; rewrite coef_poly; case: ltnP => // le_p_i; rewrite nth_default. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)