have HC : ∀ {n : ℕ}, (fun x => P.eval x)^[n + 1] t - (fun x => P.eval x)^[n] t ∈ C := by
  intro n
  rw [Cycle.mem_map, Function.iterate_succ_apply']
  exact ⟨_, iterate_mem_periodicOrbit ht n, rfl⟩
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)
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t
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)
HC : ∀ {n : ℕ}, (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t ∈ C
⊢ IsPeriodicPt (fun x => Polynomial.eval x P) 2 t