refactor(algebra): Redefine `a ≡ b [PMOD p]` (#18958)
as `∃ n : ℤ, b - a = n • p` instead of `∀ n : ℤ, b - n • p ∉ set.Ioo a (a + p)`. Since this new definition doesn't require an order on `α`, we move it to a new file `algebra.modeq`. Expand the API.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
