toIocDiv_wcovBy_toIcoDiv — Mathlib

English

The divisor toIocDiv is covariant by toIcoDiv: toIocDiv hp a b ⩿ toIcoDiv hp a b.

Русский

Делитель toIocDiv модифицируется по toIcoDiv: toIocDiv hp a b ⩿ toIcoDiv hp a b.

LaTeX

$$$ toIocDiv\\ hp\\ a\\ b \\;\\bowtie\\; toIcoDiv\\ hp\\ a\\ b $$$

Lean4

theorem toIocDiv_wcovBy_toIcoDiv (a b : α) : toIocDiv hp a b ⩿ toIcoDiv hp a b :=
  by
  suffices toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b by
    rwa [wcovBy_iff_eq_or_covBy, ← Order.succ_eq_iff_covBy]
  rw [eq_comm, ← not_modEq_iff_toIcoDiv_eq_toIocDiv, eq_comm, ← modEq_iff_toIcoDiv_eq_toIocDiv_add_one]
  exact em' _

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