Function vstd::arithmetic::div_mod::lemma_part_bound1

source · 
pub broadcast proof fn lemma_part_bound1(a: int, b: int, c: int)
Expand description
requires
0 <= a,
0 < b,
0 < c,
ensures
0 < b * c,
(b * (a / b) % (b * c)) <= b * (c - 1),

Proof that, for nonnegative integer a and positive integers b and c, the remainder of b * (a / b) divided by b * c is less than or equal to b * (c - 1). This accounts for the rounding down that occurs in integer division.