Function vstd::arithmetic::div_mod::lemma_add_mod_noop_right

source · 
pub broadcast proof fn lemma_add_mod_noop_right(x: int, y: int, m: int)
Expand description
requires
0 < m,
ensures
(x + (y % m)) % m == (x + y) % m,

Proof that describes an expanded and succinct version of modulus operator in relation to addition. Specifically, (x + (y % m)) % m == (x + y) % m.