rw [← H, sub_add_sub_cancel']
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
Hdvd : Cycle.Chain (fun x x_1 => x ∣ x_1) C
Habs :
  ∀ (m n : ℕ),
    ((fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t).natAbs =
      ((fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t).natAbs
HC' : Cycle.Chain (fun x x_1 => x = x_1) C
Heq :
  ∀ (m n : ℕ),
    (fun x => Polynomial.eval x P)^[m + 1] t - (fun x => Polynomial.eval x P)^[m] t =
      (fun x => Polynomial.eval x P)^[n + 1] t - (fun x => Polynomial.eval x P)^[n] t
n : ℕ
IH : ((fun x => Polynomial.eval x P)^[n + 1] t - t).sign = (Polynomial.eval t P - t).sign
H :
  (fun x => Polynomial.eval x P)^[n] (Polynomial.eval (Polynomial.eval t P) P) -
      (fun x => Polynomial.eval x P)^[n] (Polynomial.eval t P) =
    Polynomial.eval t P - t
⊢ ((fun x => Polynomial.eval x P)^[n] (Polynomial.eval (Polynomial.eval t P) P) - t).sign =
    ((fun x => Polynomial.eval x P)^[n] (Polynomial.eval t P) - t + (Polynomial.eval t P - t)).sign
no goals