Theorem: IMOSL.IMO2011A4.PNat_Nat_conj_iterate (IMOSLLean4/IMO2011/A4/A4.lean)

State before:
f : ℕ → ℕ
m : ℕ+
k : ℕ
⊢ (fun n => (f n.natPred).succPNat)^[k + 1] m = (f^[k + 1] m.natPred).succPNat
Tactic:
rw [iterate_succ_apply', iterate_succ_apply',
  PNat_Nat_conj_iterate f m k]
State after:
f : ℕ → ℕ
m : ℕ+
k : ℕ
⊢ (f (f^[k] m.natPred).succPNat.natPred).succPNat = (f (f^[k] m.natPred)).succPNat

State before:
f : ℕ → ℕ
m : ℕ+
k : ℕ
⊢ (f (f^[k] m.natPred).succPNat.natPred).succPNat = (f (f^[k] m.natPred)).succPNat
Tactic:
rfl
State after:
no goals