∀ {R : Type u} [inst : CommSemiring R] (p q : Polynomial R),
  Polynomial.derivative (Polynomial.eval₂ Polynomial.C q p) =
    Polynomial.eval₂ Polynomial.C q (Polynomial.derivative p) * Polynomial.derivative q