vstd::arithmetic::div_mod

Function lemma_sub_mod_noop_right

Source 
pub broadcast proof fn lemma_sub_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 subtraction. Specifically, (x - (y % m)) % m == (x - y) % m.