proposition: Lemma coef_comp_poly_Xn p n i : 0 < n -> (p \Po 'X^n)`_i = if n %| i then p`_(i %/ n) else 0.
proof: Proof. move=> n_gt0; rewrite comp_polyE; under eq_bigr do rewrite -exprM mulnC. rewrite coef_sumMXn/=; case: dvdnP => [[j ->]|nD]; last first. by rewrite big1// => j /eqP ?; case: nD; exists j. under eq_bigl do rewrite eqn_mul2r gtn_eqF//. by rewrite big_ord1_eq if_nth ?leqVgt ?mulnK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)