no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
p : R[X]
⊢ ↑derivative (p ^ 2) = ↑C 2 * p * ↑derivative p
rw [derivative_pow_succ, Nat.cast_one, one_add_one_eq_two, pow_one]