Function vstd::arithmetic::div_mod::lemma_mul_mod_noop_general

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

Proof of various properties about modulo equivalence with respect to multiplication, specifically various expressions that (x * y) % m is equivalent to.