A document about the precursor to ANDF (Architecture Neutral Distribution Format) mentions that two of its integer division/remainder primitives "are those generally implemented directly by processor instructions giving the sign of the remainder the same as the sign of the quotient" (it would be more precise to say that the sign of the non-zero remainder is positive if signs of the dividend and the divisor match, and negative otherwise). The other two primitives implement the case where the sign of remainder is the same as the sign of divisor.
Was this a misstatement (intending "dividend", as in x86), or there really was a CPU implementing this peculiar kind of integer division? None of the programming languages define their modulo operation to make the remainder to follow the sign of the quotient.
After some thought, I'm convinced that "the sign of the quotient" was a mistake in the document.
Using dimensional analysis, consider moving N ft North (positive) of South (negative) making K ft steps while facing North or South. The result is N/K full steps, where the sign of the result determines whether the steps were forwards (positive) or backwards (negative). The remainder of the distance could be either always in the same direction as were the full steps (the sign of the remainder follows the sign of the dividend), or always forwards (the sign of the remainder follows the sign of the divisor), or always to the North (the remainder is always positive). The obvious opposites are also possible but less useful.
However, the situation when the remainder of the distance would be to the North if the steps were forwards, and to the South if they were backwards, or vice versa, doesn't make sense.
(x+y+z+1)//3
). As for the guarantee you mention, the only use I can think of for it...