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.