mathlib

645b6de4 - refactor(algebra/order/to_interval_mod): Negate the definition of `mem_Ioo_mod` (#18912)

refactor(algebra/order/to_interval_mod): Negate the definition of `mem_Ioo_mod` (#18912) This replaces `mem_Ioo_mod hp a b` with `¬add_comm_group.modeq p a b`. This is more consistent with `int.modeq`, `nat.modeq`, and `smodeq`. There's still some duplication here, but at least these four ideas are now conceptually aligned. This remove any lemmas of the form `¬modeq p a b ↔ _ ≠ _` as these are now trivial consequences of the `modeq p a b ↔ _ = _` versions,