have hPab : (P + (X : ℤ[X]) - a - b).natDegree = P.natDegree := by
  rw [sub_sub, ← Int.cast_add]
  have h₁ : (P + X).natDegree = P.natDegree := by
    rw [natDegree_add_eq_left_of_natDegree_lt]
    simpa using hP
  rwa [natDegree_sub_eq_left_of_natDegree_lt]
  rw [h₁, natDegree_intCast]
  exact zero_lt_one.trans hP
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree
case neg.intro.intro
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
H : ¬(P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
a : ℤ
b : ℤ := Polynomial.eval a P
hab : ¬b = a
ha : Polynomial.eval b P = a
hPab : (P + X - ↑a - ↑b).natDegree = P.natDegree
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree