Cancel the leading terms of two polynomials
cancel_leads p q: the polynomial formed by multiplying
qby monomials so that they have the same leading term, and then subtracting.
The degree of
cancel_leads is less than that of the larger of the two polynomials being cancelled.
Thus it is useful for induction or minimal-degree arguments.
cancel_leads p q is formed by multiplying
q by monomials so that they
have the same leading term, and then subtracting.