have hPX' : P - X ≠ 0 := by
  intro h
  rw [h, natDegree_zero] at hPX
  rw [← hPX] at hP
  exact (zero_le_one.not_lt hP).elim
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree
P : ℤ[X]
hP : 1 < P.natDegree
hPX : (P - X).natDegree = P.natDegree
hPX' : P - X ≠ 0
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree