nat.modeq

Modular equality. modeq n a b, or a ≡ b [MOD n], means that a - b is a multiple of n.