---

Step * 1 of Lemma geo-add-length_functionality_wrt_lt


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

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

---

Latex:

---

Latex:

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


By

---

Latex:
(RWO    "6<  -1<"  0  THENA  Auto)

---

Home Index