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