---

Step * of Lemma rem_bounds_absval_le

∀b:ℤ-o. ∀a:ℤ.  (|a rem b| ≤ |b|)
BY
{ (InstLemma `rem_bounds_absval` [] THEN RepeatFor 2 (ParallelLast) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}b:\mBbbZ{}\msupminus{}\msupzero{}.  \mforall{}a:\mBbbZ{}.    (|a  rem  b|  \mleq{}  |b|)


By

---

Latex:
(InstLemma  `rem\_bounds\_absval`  []  THEN  RepeatFor  2  (ParallelLast)  THEN  Auto)

---

Home Index