proposition: Lemma derivM p q : (p * q)^`() = p^`() * q + p * q^`().
proof: Proof. elim/poly_ind: p => [|p b IHp]; first by rewrite !(mul0r, add0r, derivC). rewrite mulrDl -mulrA -commr_polyX mulrA -[_ * 'X]addr0 raddfD /= !derivMXaddC. by rewrite deriv_mulC IHp !mulrDl -!mulrA !commr_polyX !addrA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)