---

Step * of Lemma general_arith_equation1

∀[b:ℤ]. ∀[a,c:Top].  ((a - b) + c ~ (a + c) - b)
BY
{ ((UnivCD THENA Auto) THEN Unfold `subtract` 0 THEN (RWO "add-associates" 0 THENA Auto) THEN EqCD THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[b:\mBbbZ{}].  \mforall{}[a,c:Top].    ((a  -  b)  +  c  \msim{}  (a  +  c)  -  b)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `subtract`  0
  THEN  (RWO  "add-associates"  0  THENA  Auto)
  THEN  EqCD
  THEN  Auto)

---

Home Index