Function vstd::arithmetic::div_mod::lemma_mod_adds
source · pub broadcast proof fn lemma_mod_adds(a: int, b: int, d: int)
Expand description
requires
0 < d,
ensuresa % d + b % d == (a + b) % d + d * ((a % d + b % d) / d),
(a % d + b % d) < d ==> a % d + b % d == (a + b) % d,
Proof of two properties of the sum of two remainders with the same dividend:
a % d + b % d == (a + b) % d + d * ((a % d + b % d) / d)
.(a % d + b % d) < d ==> a % d + b % d == (a + b) % d
.