Function vstd::arithmetic::div_mod::lemma_dividing_sums
source · pub broadcast proof fn lemma_dividing_sums(a: int, b: int, d: int, r: int)Expand description
requires
0 < d,r == a % d + b % d - (a + b) % d,d * ((a + b) / d) - r == d * (a / d) + d * (b / d),Proof that, given r == a % d + b % d - (a + b) % d, r can also
be expressed as d * ((a + b) / d) - d * (a / d) - d * (b / d)