Description: The degree of a product of polynomials is at most the sum of degrees. (Contributed by Mario Carneiro, 24-Jul-2014)