proposition: Lemma deriv_comp p q : (p \Po q) ^`() = (p ^`() \Po q) * q^`().
proof: Proof. elim/poly_ind: p => [|p c IHp]; first by rewrite !(deriv0, comp_poly0) mul0r. rewrite comp_poly_MXaddC derivD derivC derivM IHp derivMXaddC comp_polyD. by rewrite comp_polyM comp_polyX addr0 addrC mulrAC -mulrDl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)