Strict polynomial error decrease from nonvanishing derivatives (source code)

= Strict polynomial error decrease from nonvanishing derivatives
{title2=$E_{n-1}(f)>E_n(f)$}

If $n\ge1$, $f$ is real and $C^n$ on an interval, and $f^{(n)}$ is nowhere zero there, the displayed inequality holds. If the errors were equal, a best degree-at-most-$n-1$ polynomial would also be best at degree $n$. The <Chebyshev alternation theorem> and <intermediate value theorem> would give $n+1$ zeros of the error. Applying <Rolle's theorem> $n$ times would force a zero of $f^{(n)}$, a contradiction. The zero-error case already contradicts $f^{(n)}\ne0$. In particular this proves strict improvement for the <exponential function> at every positive degree step.