simp [deriv_const_mul]
case succ.h
r : ℝ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (r • f) = r • iteratedDeriv n f
x : ℝ
⊢ deriv (fun x => (r • iteratedDeriv n f) x) x = (r • deriv (iteratedDeriv n f)) x
no goals