congr
case neg.a.inr
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : i ≤ (derivative p).natDegree
⊢ (derivative p).coeff i * r ^ (p.natDegree - (i + 1)) =
    (derivative p).coeff i * r ^ ((derivative p).natDegree - i + (p.natDegree - ((derivative p).natDegree + 1)))
case neg.a.inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : i ≤ (derivative p).natDegree
⊢ p.natDegree - (i + 1) = (derivative p).natDegree - i + (p.natDegree - ((derivative p).natDegree + 1))