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),#[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.