mathlib

b2d7b50d - chore(algebra/order/to_interval_mod): Reorder arguments (#18908)

chore(algebra/order/to_interval_mod): Reorder arguments (#18908) The current argument order to `to_Ixx_mod` is a bit poor: In `to_Ico a hb x`, `a` and `x` play a similar role while `b` is completely separate. This PR changes this to `to_Ico hp a b`, where the translation is as follows: * `mem_Ioo_mod a p b` → `mem_Ioo_mod p a b` (this is more consistent with `int.modeq p a b`) * `to_Ico_div a hp b` → `to_Ico_div hp a b` * `to_Ioc_div a hp b` → `to_Ioc_div hp a b` * `to_Ico_mod a hp b` → `to_Ico_mod hp a b` * `to_Ioc_mod a hp b` → `to_Ioc_mod hp a b` While it might be tempting to order`to_Ico_div hp a b` as `to_Ico_div b a hp` to match the order of the morally equivalent `(b - a) / p + a`, we opt for the simpler convention of being consistent with `mem_Ioo_mod`, as in downstream files we also find it convenient to have `b` as the last argument. Generally speaking, the variables have been renamed to * `a` → `a` (the left end) * `b` → `p` (the period) * `x` → `b` (the interval length) * `y` → `c` (additional argument similar to the left end and interval length) * `z` → `n` (the euclidean dividend) Proofs are golfed slightly. The only lemma statements that changed are `to_Ico_div_eq_of_sub_zsmul_mem_Ico`/`to_Ioc_div_eq_of_sub_zsmul_mem_Ioc` that now state `to_Ico_div hp a b = n` rather than `n = to_Ico_div hp a b` (they were always used in this new direction).