---

Step * of Lemma general_arith_equation2

∀[b:ℤ]. ∀[a,c:Top].  ((a - b - c) + b ~ a - c)
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `subtract` 0
   THEN (RWO "add-associates" 0 THENA Auto)
   THEN (RW (AddrC [1;2] (RevLemmaC `add-commutes`)) 0 THENA Auto)
   THEN (RWO "add-associates<" 0 THENA Auto)) }

1
1. b : ℤ
2. a : Top
3. c : Top
⊢ ((a + (-b)) + b) + (-c) ~ a + (-c)

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `subtract`  0
  THEN  (RWO  "add-associates"  0  THENA  Auto)
  THEN  (RW  (AddrC  [1;2]  (RevLemmaC  `add-commutes`))  0  THENA  Auto)
  THEN  (RWO  "add-associates<"  0  THENA  Auto))

---

Home Index