Function vstd::arithmetic::div_mod::lemma_mod_mul_equivalent

source · 
pub broadcast proof fn lemma_mod_mul_equivalent(x: int, y: int, z: int, m: int)
Expand description
requires
m > 0,
is_mod_equivalent(x, y, m),
ensures
#[trigger] is_mod_equivalent(x * z, y * z, m),

Proof that if is_mod_equivalent holds for x, y, and m, then it holds for x * z, y * z, and m