Theorem: IMOSL.IMO2013A5.iter_four_eq (IMOSLLean4/IMO2013/A5/A5.lean)

State before:
f : ℕ → ℕ
h : good f
n : ℕ
⊢ f^[4] (n + 1) = f^[4] n + 1
Tactic:
rw [f.iterate_succ_apply, h, ← h n, ← f.iterate_succ_apply']
State after:
no goals

State before:
f : ℕ → ℕ
h : good f
h0 : ∀ (n : ℕ), f^[4] (n + 1) = f^[4] n + 1
n : ℕ
h1 : f^[4] n = f^[4] 0 + n
⊢ f^[4] n.succ = f^[4] 0 + n.succ
Tactic:
rw [Nat.add_succ, h0, h1]
State after:
no goals