---

Step * of Lemma geo-add-length-implies-eq-zero

∀[e:BasicGeometry]. ∀[x,y:Length].  y = 0 ∈ Length supposing x = x + y ∈ Length
BY
{ (Auto
   THEN (Assert x + X = x + y ∈ Length BY
               Auto)
   THEN Fold `geo-zero-length` (-1)
   THEN FLemma  `geo-add-length-cancel-left` [-1]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[e:BasicGeometry].  \mforall{}[x,y:Length].    y  =  0  supposing  x  =  x  +  y


By

---

Latex:
(Auto
  THEN  (Assert  x  +  X  =  x  +  y  BY
                          Auto)
  THEN  Fold  `geo-zero-length`  (-1)
  THEN  FLemma    `geo-add-length-cancel-left`  [-1]
  THEN  Auto)

---

Home Index