proposition: Lemma comp_polyA p q r : p \Po (q \Po r) = (p \Po q) \Po r.
proof: Proof. elim/poly_ind: p => [|p c IHp]; first by rewrite !comp_polyC. by rewrite !comp_polyD !comp_polyM !comp_polyX IHp !comp_polyC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)