mathlib

a993e7ee - feat(algebra/order/to_interval_mod): more relations between `to_Ixx_{mod/div}` definitions (#17933)

feat(algebra/order/to_interval_mod): more relations between `to_Ixx_{mod/div}` definitions (#17933) `to_Ico_div` and `to_Ioc_div` differ by at most 1, and the modulo versions differ by at most `b`. This also renames some lemmas that have the wrong name.