∀ {R : Type u} [inst : Semiring R] {n : ℕ} (p q : Polynomial R),
  (⇑Polynomial.derivative)^[n] (p * q) =
    ∑ k ∈ Finset.range n.succ, n.choose k • ((⇑Polynomial.derivative)^[n - k] p * (⇑Polynomial.derivative)^[k] q)