---

Step * 1 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 + |ab| + y
BY
{ (BLemma `geo-le_weakening` THEN Auto) }

---

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  +  |ab|  +  y


By

---

Latex:
(BLemma  `geo-le\_weakening`  THEN  Auto)

---

Home Index