Function vstd::arithmetic::div_mod::is_mod_equivalent

source · 
pub open spec fn is_mod_equivalent(x: int, y: int, m: int) -> bool
Expand description
recommends
m > 0,
{ x % m == y % m <==> (x - y) % m == 0 }

This function says that x is congruent to y modulo m if and only if their difference x - y is congruent to 0 modulo m.