vstd::arithmetic::div_mod

Function lemma_mod_breakdown

Source 
pub broadcast proof fn lemma_mod_breakdown(x: int, y: int, z: int)
Expand description
requires
0 <= x,
0 < y,
0 < z,
ensures
y * z > 0,
x % (y * z) == y * ((x / y) % z) + x % y,

Proof of the validity of an expanded form of the modulus operation. Specifically, x % (y * z) == y * ((x / y) % z) + x % y.