Limits related to polynomial and rational functions #
This file proves basic facts about limits of polynomial and rationals functions.
The main result is
eval_is_equivalent_at_top_eval_lead, which states that for
P of degree
n with leading coefficient
a, the corresponding
polynomial function is equivalent to
a * x^n as
x goes to +∞.
We can then use this result to prove various limits for polynomial and rational functions, depending on the degrees and leading coefficients of the considered polynomials.