Description:

• When both a and b are constants, div(a,b) computes floor(a / b). In other words, it returns the quotient of the Euclidian division of a by b.
• When both a and b are polynomials with at least one being non-constant, div(a,b) computes a polynomial q such that the polynomial r equal to a - q * b is of degree strictly smaller than the degree of b (see exception below). In order to recover r, use the mod command.
• div works on polynomials whose coefficients are constant expressions that cannot be simplified (by the tool) to rational numbers. In most cases, the tool is able to perform the Euclidian polynomial division for such polynomials and stop the Euclidian division algorithm only when r is of degree strictly smaller than the degree of b. In certain cases, when the polynomials involve coefficients given as constant expressions that are mathematically zero but for which the tool is unable to detect this fact, the tool may be unable to correctly determine that r is actually of degree stricly smaller than the degree of b. The issue arises in particular for polynomials whose leading coefficient is a constant expression which is zero without the tool being able to detect this. In these cases, div, together with mod, just guarantee that q and r, as returned by the two commands, satisfy that r added to the product of q and b yields a, and that r is of the smallest degree the tool can admit. However, there might exist another pair of a quotient and remainder polynomial for which the remainder polynomial is of a degree less than the one of r.
• When at least one of a or b is a function that is no polynomial, div(a,b) returns 0.