---

Step * of Lemma rem_sym_2

No Annotations
∀[a:ℤ]. ∀[n:ℤ-o].  ((a rem n) = (a rem -n) ∈ ℤ)
BY
{ (InstLemma `rem_sym` [] 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\_sym`  []  THEN  RepeatFor  2  (ParallelLast))

---

Home Index