---

Step * 1 of Lemma geo-add-length-cancel-left-lt3


1. e : BasicGeometry
2. y : Length
3. z : Length
4. z < 0 + y
⊢ z < y
BY
{ ((InstLemma `geo-add-length-cancel-left-lt` [⌜e⌝;⌜z⌝;⌜y⌝;⌜0⌝]⋅ THEN Auto)
   THEN (Assert 0 + z = z ∈ Length BY
               EAuto 1)
   THEN RWO "-1" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  y  :  Length
3.  z  :  Length
4.  z  <  0  +  y
\mvdash{}  z  <  y


By

---

Latex:
((InstLemma  `geo-add-length-cancel-left-lt`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (Assert  0  +  z  =  z  BY
                          EAuto  1)
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index