Function vstd::arithmetic::div_mod::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,(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.