Function vstd::arithmetic::div_mod::lemma_sub_mod_noop

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

Proof that modulo distributes over subtraction provided you do an extra modulo operation after subtracting the remainders. Specifically, ((x % m) - (y % m)) % m == (x - y) % m.