Function vstd::arithmetic::div_mod::lemma_add_mod_noop
source · pub broadcast proof fn lemma_add_mod_noop(x: int, y: int, m: int)Expand description
requires
0 < m,((x % m) + (y % m)) % m == (x + y) % m,Proof that modulo distributes over addition, provided you do an
extra modulo after adding the remainders. Specifically,
((x % m) + (y % m)) % m == (x + y) % m.