Function vstd::arithmetic::div_mod::lemma_mod_multiples_vanish

source · 
pub broadcast proof fn lemma_mod_multiples_vanish(a: int, b: int, m: int)
Expand description
requires
0 < m,
ensures
#[trigger] ((m * a + b) % m) == b % m,

Proof that adding any multiple of the divisor to the dividend will produce the same remainder. In other words, (m * a + b) % m == b % m.