---

Step * of Lemma rem_sym

No Annotations
∀[a:ℤ]. ∀[b:ℤ-o].  ((a rem -b) = (a rem b) ∈ ℤ)
BY
{ (Auto THEN (Decide ⌜0 ≤ b⌝ THENA Auto)) }

1
1. a : ℤ
2. b : ℤ-o
3. 0 ≤ b
⊢ (a rem -b) = (a rem b) ∈ ℤ

2
1. a : ℤ
2. b : ℤ-o
3. ¬(0 ≤ b)
⊢ (a rem -b) = (a rem b) ∈ ℤ

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (Decide  \mkleeneopen{}0  \mleq{}  b\mkleeneclose{}  THENA  Auto))

---

Home Index