Monotonicity of polynomial evaluation

Over a canonically ordered semiring (such as ℕ), every coefficient of a polynomial is nonnegative, so evaluation of the polynomial is a monotone function. This is useful for reasoning about polynomial time bounds.

theorem Polynomial.monotone_eval {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [CanonicallyOrderedAdd R] (p : Polynomial R) : Monotone fun (x : R) => eval x p

Over a canonically ordered semiring, evaluation of a polynomial is monotone.

theorem Polynomial.eval_mono {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [CanonicallyOrderedAdd R] (p : Polynomial R) {a b : R} (hab : a ≤ b) : eval a p ≤ eval b p

Over a canonically ordered semiring, evaluation of a polynomial preserves ≤.