Commit 2023-01-10 09:28 e017e666

refactor(algebra/order/to_interval_mod): state more results in terms of interval sets (#18102) Since the declarations contain Ioc or Ico in their name, I would argue the statements are clearer if expressed with the corresponding sets rather than with inequalities. While this makes a few proofs longer in terms of characters, they're shorter in terms of terms.