Function vstd::arithmetic::div_mod::lemma_truncate_middle

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

Proof that common factors from the dividend and divisor of a modulus operation can be factored out. Specifically, (b * x) % (b * c) == b * (x % c).