mathlib3

e017e666 - refactor(algebra/order/to_interval_mod): state more results in terms of interval sets (#18102)

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.