Function vstd::arithmetic::div_mod::lemma_mod_mod

source · 
pub broadcast proof fn lemma_mod_mod(x: int, a: int, b: int)
Expand description
requires
0 < a,
0 < b,
ensures
0 < a * b,
(x % (a * b)) % a == x % a,

Proof that the remainder when x is divided by a * b, taken modulo a, is equivalent to x modulo a. That is, (x % (a * b)) % a == x % a.