rw [h]
case succ
r : ℝ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (r • f) = r • iteratedDeriv n f
⊢ deriv (iteratedDeriv n (r • f)) = r • deriv (iteratedDeriv n f)
case succ
r : ℝ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (r • f) = r • iteratedDeriv n f
⊢ deriv (r • iteratedDeriv n f) = r • deriv (iteratedDeriv n f)