---

Step * of Lemma geo-add-length-cancel-right-lt

∀[e:BasicGeometry]. ∀[x,y,z:Length].  (z + x < y + x ⇒ z < y)
BY
{ (Auto
   THEN ((Assert z + x = x + z ∈ Length BY Auto) THEN RWO  "-1" 5 THEN Auto)
   THEN (Assert y + x = x + y ∈ Length BY
               Auto)
   THEN (RWO  "-1" 5 THEN Auto)
   THEN FLemma `geo-add-length-cancel-left-lt` [5]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[e:BasicGeometry].  \mforall{}[x,y,z:Length].    (z  +  x  <  y  +  x  {}\mRightarrow{}  z  <  y)


By

---

Latex:
(Auto
  THEN  ((Assert  z  +  x  =  x  +  z  BY  Auto)  THEN  RWO    "-1"  5  THEN  Auto)
  THEN  (Assert  y  +  x  =  x  +  y  BY
                          Auto)
  THEN  (RWO    "-1"  5  THEN  Auto)
  THEN  FLemma  `geo-add-length-cancel-left-lt`  [5]
  THEN  Auto)

---

Home Index