Theorem: IMOSL.IMO2017A3.iterate_add_mul_eq (IMOSLLean4/IMO2017/A3/A3.lean)

State before:
n k : ℕ
S : Type u_1
f : S → S
h : f^[n + k] = f^[n]
t : ℕ
⊢ f^[n + k * (t + 1)] = f^[n]
Tactic:
rw [k.mul_succ, ← Nat.add_assoc, f.iterate_add,
iterate_add_mul_eq h t, ← f.iterate_add, h]
State after:
no goals