Function vstd::arithmetic::div_mod::lemma_breakdown
source · pub broadcast proof fn lemma_breakdown(x: int, y: int, z: int)Expand description
requires
0 <= x,0 < y,0 < z,0 < y * z,(x % (y * z)) == y * ((x / y) % z) + x % y,The remainder of a nonnegative integer x divided by the product of two positive integers
y and z is equivalent to dividing x by y, dividing the quotient by z, multiplying
the remainder by y, and then adding the product to the remainder of x divided by y.
In mathematical terms, (x % (y * z)) == y * ((x / y) % z) + x % y.