---

Step * of Lemma rem_2_to_1

∀[a:{...0}]. ∀[n:ℕ+].  ((a rem n) = (-(-a rem n)) ∈ ℤ)
BY
{ ((UnivCD THENA Auto) THEN (RWH (LemmaC `rem_to_div`) 0 THENA Auto)) }

1
1. a : {...0}
2. n : ℕ+
⊢ (a - (a ÷ n) * n) = (-((-a) - ((-a) ÷ n) * n)) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[a:\{...0\}].  \mforall{}[n:\mBbbN{}\msupplus{}].    ((a  rem  n)  =  (-(-a  rem  n)))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RWH  (LemmaC  `rem\_to\_div`)  0  THENA  Auto))

---

Home Index