cases lt_or_le (natDegree (derivative p)) i with
| inl h => simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul]
| inr h =>
  congr
  have h' := natDegree_derivative_lt hp
  zify
  rw [Int.ofNat_sub h', Int.ofNat_sub h, Int.ofNat_sub (h.trans_lt h')]
  simp only [Nat.cast_succ]
  abel
case neg.a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
⊢ (derivative p).coeff i * r ^ (p.natDegree - (i + 1)) =
    (derivative p).coeff i * r ^ ((derivative p).natDegree - i + (p.natDegree - ((derivative p).natDegree + 1)))
no goals