Function vstd::arithmetic::div_mod::lemma_indistinguishable_quotients
source · pub broadcast proof fn lemma_indistinguishable_quotients(a: int, b: int, d: int)Expand description
requires
0 < d,0 <= a - a % d <= b < a + d - a % d,a / d == b / d,Proof that for a positive integer d, if a - a % d is less than
or equal to b and b is less than a + d - a % d, then the
quotient of a divided by d is equivalent to the quotient of
b divided by d.
In other words, if a and b occur between the same two
multiples of d, then their quotient with d is equivalent.