rw [natDegree_add_eq_left_of_natDegree_lt]
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 + X).natDegree = P.natDegree
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
⊢ X.natDegree < P.natDegree