∀ {R : Type u_2} [inst : CommRing R] [IsDomain R] [inst_2 : DecidableEq R] [inst_3 : Fintype R] {p : Polynomial R},
  0 < p.degree → Fintype.card R ≤ p.natDegree * (Finset.image (fun x => Polynomial.eval x p) Finset.univ).card