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.