toIocMod_le_toIcoMod_add — Mathlib

English

The IocMod value is at most the IcoMod value plus p: toIocMod hp a b ≤ toIcoMod hp a b + p.

Русский

Значение IocMod не превосходит значение IcoMod плюс p: toIocMod hp a b ≤ toIcoMod hp a b + p.

LaTeX

$$$ toIocMod\\ hp\\ a\\ b \\le toIcoMod\\ hp\\ a\\ b + p $$$

Lean4

theorem toIocMod_le_toIcoMod_add (a b : α) : toIocMod hp a b ≤ toIcoMod hp a b + p :=
  by
  rw [toIcoMod, toIocMod, sub_add, sub_le_sub_iff_left, sub_le_iff_le_add, ← add_one_zsmul,
    (zsmul_left_strictMono hp).le_iff_le]
  apply (toIocDiv_wcovBy_toIcoDiv _ _ _).le_succ

Похожие утверждения