Definitions of division for binary integers, Euclid convention.
In this convention, the remainder is always positive.
For other conventions, see
Z.div and
Z.quot in file
BinIntDef.
To avoid collision with the other divisions, we place this one
under a module.