Function vstd::arithmetic::div_mod::lemma_mul_mod_noop_left

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

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