Function vstd::arithmetic::div_mod::lemma_mul_mod_noop
source · pub broadcast proof fn lemma_mul_mod_noop(x: int, y: int, m: int)Expand description
requires
0 < m,(x % m) * (y % m) % m == #[trigger] ((x * y) % m),Proof that modulo distributes over multiplication, provided you do
an extra modulo operation after multiplying the remainders. Specifically,
(x % m) * (y % m) % m == (x * y) % m.