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

State before:
f : ℕ → ℕ
h : good f
n : ℕ
⊢ f^[4] n = n + 4
Tactic:
rw [iter_four_eq h, add_comm, iter_four_zero_eq_four h]
State after:
no goals