conv => rhs; rw [iteratedDeriv_succ]
case succ
r : ℝ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (r • f) = r • iteratedDeriv n f
⊢ iteratedDeriv (Nat.succ n) (r • f) = r • iteratedDeriv (Nat.succ n) f
case succ
r : ℝ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (r • f) = r • iteratedDeriv n f
⊢ iteratedDeriv (Nat.succ n) (r • f) = r • deriv (iteratedDeriv n f)