proposition: Lemma comp_poly_Xn p n : 0 < n -> p \Po 'X^n = \poly_(i < size p * n) if n %| i then p`_(i %/ n) else 0.
proof: Proof. move=> n_gt0; apply/polyP => i; rewrite coef_comp_poly_Xn // coef_poly. case: dvdnP => [[k ->]|]; last by rewrite if_same. by rewrite mulnK // ltn_mul2r n_gt0 if_nth ?leqVgt. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)