rw [Cycle.mem_map, Function.iterate_succ_apply']
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
n : ℕ
⊢ (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
P : ℤ[X]
t : ℤ
ht : t ∈ periodicPts fun x => Polynomial.eval x P
C : Cycle ℤ := Cycle.map (fun x => Polynomial.eval x P - x) (periodicOrbit (fun x => Polynomial.eval x P) t)
n : ℕ
⊢ ∃ a ∈ periodicOrbit (fun x => Polynomial.eval x P) t,
    Polynomial.eval a P - a =
      Polynomial.eval ((fun x => Polynomial.eval x P)^[n] t) P - (fun x => Polynomial.eval x P)^[n] t