---

Step * of Lemma radd-rminus

∀[x:ℝ]. ((x + -(x)) = r0)
BY
{ (Auto
   THEN (BLemma `req-iff-bdd-diff` THENA Auto)
   THEN Unfold `radd` 0
   THEN (RWO "accelerate-bdd-diff" 0⋅ THENA Auto)
   THEN (RWO "reg-seq-list-add-as-l_sum" 0 THENA Auto)) }

1
1. x : ℝ
⊢ bdd-diff(λn.l_sum(map(λx.(x n);[x; -(x)]));r0)

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  ((x  +  -(x))  =  r0)


By

---

Latex:
(Auto
  THEN  (BLemma  `req-iff-bdd-diff`  THENA  Auto)
  THEN  Unfold  `radd`  0
  THEN  (RWO  "accelerate-bdd-diff"  0\mcdot{}  THENA  Auto)
  THEN  (RWO  "reg-seq-list-add-as-l\_sum"  0  THENA  Auto))

---

Home Index