Modular equality. modeq n a b, or a ≡ b [MOD n], means
that a - b is a multiple of n.
modeq n a b
a ≡ b [MOD n]
a - b
A variant of modeq_iff_dvd with nat divisibility
The natural number less than n*m congruent to a mod n and b mod m