Commit 2023-05-03 03:14 645b6de4

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,