Function vstd::arithmetic::div_mod::lemma_mul_mod_noop_right

source · 
pub broadcast proof fn lemma_mul_mod_noop_right(x: int, y: int, m: int)
Expand description
requires
0 < m,
ensures
x * (y % m) % m == #[trigger] ((x * y) % m),

Proof that the remainder when x * y is divided by m is equivalent to the remainder when x * (y % m) is divided by m.