rw [natDegree_eq_zero_iff_degree_le_zero, degree_le_zero_iff] at hp
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
case pos
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : p = C (p.coeff 0)
⊢ derivative (p.scaleRoots r) = (derivative p).scaleRoots r