English
For any a,b the IcoMod value is not greater than the corresponding IocMod value: toIcoMod hp a b ≤ toIocMod hp a b.
Русский
Для любых a,b значение IcoMod не превосходит соответствующее значение IocMod: toIcoMod hp a b ≤ toIocMod hp a b.
LaTeX
$$$ toIcoMod\\ hp\\ a\\ b \\leq toIocMod\\ hp\\ a\\ b $$$
Lean4
theorem toIcoMod_le_toIocMod (a b : α) : toIcoMod hp a b ≤ toIocMod hp a b :=
by
rw [toIcoMod, toIocMod, sub_le_sub_iff_left]
exact zsmul_left_mono hp.le (toIocDiv_wcovBy_toIcoDiv _ _ _).le