mathlib

a0ed43b3 - fix(algebra/order/to_interval_mod): align `to_Ico_div` with regular division (#18105)

fix(algebra/order/to_interval_mod): align `to_Ico_div` with regular division (#18105) The previous definition of `to_Ico_div` and `to_Ico_mod` had `x = to_Ico_mod a hb x - to_Ico_div a hb x • b`; but the usual convention for div and mod is `x = x / b + x % b • b`. This change flips the sign, and adjust all the lemmas accordingly. As a result, we now have the more natural `to_Ico_div a hb x = ⌊(x - a) / b⌋` instead of the previous `to_Ico_div a hb x = -⌊(x - a) / b⌋`. This also changes ```diff def mem_Ioo_mod (b x : α) : Prop := -∃ z : ℤ, x + z • b ∈ set.Ioo a (a + b) +∃ z : ℤ, x - z • b ∈ set.Ioo a (a + b) ``` even though the two are equivalent; because this means that `z` corresponds to `to_Ico_div `.