div package:incipit-base

integer division truncated toward negative infinity
Division (round down) of natural numbers. Div x 0 is undefined (i.e., it cannot be reduced).
simultaneous div and mod
Generalisation of div to any instance of Real
Generalisation of divMod to any instance of Real