Function vstd::arithmetic::div_mod::lemma_mod_equivalence
source · pub broadcast proof fn lemma_mod_equivalence(x: int, y: int, m: int)Expand description
requires
0 < m,x % m == y % m <==> (x - y) % m == 0,Proof that x and y are congruent modulo m if and only if `x
- y
is congruent to 0 modulom. In other words,x % m == y % m <==> (x - y) % m == 0`.
Note: The Dafny standard library uses the triggers x % m, y % m
for the broadcasted forall quantifier. But this can lead to a trigger loop,
so we don’t do that here.