mathlib3

4c8f86bd - feat(algebra/order/to_interval_mod): symmetric variants of lemmas (#18942)

feat(algebra/order/to_interval_mod): symmetric variants of lemmas (#18942) These lemmas are about expressions in the second instead of third arguments of the `I{co,oc}_{mod,div}` functions. Some existing lemmas clashed with these new lemmas; they have been renamed as follows: * `to_Ico_div_sub'` → `to_Ico_div_sub_eq_to_Ico_div_add` * `to_Ioc_div_sub'` → `to_Ioc_div_sub_eq_to_Ioc_div_add` * `to_Ico_div_add_right'` → `to_Ico_div_sub_eq_to_Ico_div_add'` (and reversed) * `to_Ioc_div_add_right'` → `to_Ioc_div_sub_eq_to_Ioc_div_add'` (and reversed) * `to_Ico_mod_sub'` → `to_Ico_mod_sub_eq_sub` * `to_Ioc_mod_sub'` → `to_Ioc_mod_sub_eq_sub` * `to_Ico_mod_add_right'` → `to_Ico_mod_add_right_eq_add` * `to_Ioc_mod_add_right'` → `to_Ioc_mod_add_right_eq_add` The statement of `to_Ioc_div_zsmul_add` is commuted to be consistent with the lemmas around it; presumably it was a copy-and-paste error.