by_cases H : (P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
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
case pos
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
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree

case neg
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
⊢ (P.comp P - X).roots.toFinset.card ≤ P.natDegree