---

Step * of Lemma rem_sym_1

No Annotations
∀[a:ℤ]. ∀[n:ℤ-o].  ((-(a rem n)) = (-a rem n) ∈ ℤ)
BY
{ (InstLemma `rem_antisym` [] THEN RepeatFor 2 (ParallelLast')) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[a:\mBbbZ{}].  \mforall{}[n:\mBbbZ{}\msupminus{}\msupzero{}].    ((-(a  rem  n))  =  (-a  rem  n))


By

---

Latex:
(InstLemma  `rem\_antisym`  []  THEN  RepeatFor  2  (ParallelLast'))

---

Home Index