Theorem: RuesNMthIteratedDeriv (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
n m : ℕ+
⊢ iteratedDeriv (↑m) (Rues n) = RuesDiff n ↑↑m
Tactic:
rw [←RuesDiffM0EqualsRues, RuesDiffIteratedDeriv]
State after:
n m : ℕ+
⊢ RuesDiff n (↑↑m + 0) = RuesDiff n ↑↑m

State before:
n m : ℕ+
⊢ RuesDiff n (↑↑m + 0) = RuesDiff n ↑↑m
Tactic:
simp only [add_zero]
State after:
no goals