∀ {R : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (P : Polynomial R)
  {a b : S}, IsNilpotent (a - b) → IsNilpotent ((Polynomial.aeval a) P - (Polynomial.aeval b) P)