Erase the leading term of a univariate polynomial #
erase_lead f: the polynomial
f - leading term of f
erase_lead serves as reduction step in an induction, shaving off one monomial from a polynomial.
The definition is set up so that it does not mention subtraction in the definition,
and thus works for polynomials over semirings as well as rings.
An induction lemma for polynomials. It takes a natural number
N as a parameter, that is
required to be at least as big as the
nat_degree of the polynomial. This is useful to prove
results where you want to change each term in a polynomial to something else depending on the
nat_degree of the polynomial itself and not on the specific
nat_degree of each term.