---

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


1. [e] : BasicGeometry
2. [x] : Length
3. [y] : Length
4. [z] : Length
5. a : Point
6. b : Point
7. a ≠ b
8. z + x + |ab| ≤ z + y
⊢ x + |ab| ≤ y
BY
{ (RWO "geo-add-length-assoc<" (-1) THENA Auto) }

1
1. [e] : BasicGeometry
2. [x] : Length
3. [y] : Length
4. [z] : Length
5. a : Point
6. b : Point
7. a ≠ b
8. z + x + |ab| ≤ z + y
⊢ x + |ab| ≤ y

---

Latex:

---

Latex:

1.  [e]  :  BasicGeometry
2.  [x]  :  Length
3.  [y]  :  Length
4.  [z]  :  Length
5.  a  :  Point
6.  b  :  Point
7.  a  \mneq{}  b
8.  z  +  x  +  |ab|  \mleq{}  z  +  y
\mvdash{}  x  +  |ab|  \mleq{}  y


By

---

Latex:
(RWO  "geo-add-length-assoc<"  (-1)  THENA  Auto)

---

Home Index