Function vstd::arithmetic::div_mod::lemma_mod_sub_multiples_vanish

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

Proof that subtracting the divisor from the dividend doesn’t change the remainder. Specifically, (-m + b) % m == b % m.