rw [hp, Nat.zero_sub, pow_zero, one_smul]
case pos
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : p.natDegree = 0
⊢ derivative (p.scaleRoots r) = r ^ (p.natDegree - ((derivative p).natDegree + 1)) • (derivative p).scaleRoots r
case pos
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : p.natDegree = 0
⊢ derivative (p.scaleRoots r) = (derivative p).scaleRoots r