vstd::arithmetic::div_mod

Function lemma_mod_adds

Source 
pub broadcast proof fn lemma_mod_adds(a: int, b: int, d: int)
Expand description
requires
0 < d,
ensures
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,

Proof of two properties of the sum of two remainders with the same dividend:

  1. a % d + b % d == (a + b) % d + d * ((a % d + b % d) / d).
  2. (a % d + b % d) < d ==> a % d + b % d == (a + b) % d.