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,
ensures
x % m == y % m <==> (x - y) % m == 0,

Proof that x and y are congruent modulo m if and only if `x

  • yis 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.