∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {p : Polynomial R}
  {n : ℕ}, p.natDegree < n → ∀ (x : S), (Polynomial.aeval x) p = ∑ i ∈ Finset.range n, p.coeff i • x ^ i