---

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


1. e : BasicGeometry
2. a : Point
3. O_X_a
4. b : Point
5. O_X_b
6. c : Point
7. O_X_c
8. c + a ≤ c + b
⊢ Ax ∈ a ≤ b
BY
{ (Unfold `geo-le` -1 THEN SqExRepD) }

1
1. e : BasicGeometry
2. a : Point
3. O_X_a
4. b : Point
5. O_X_b
6. c : Point
7. O_X_c
8. p' : {p:Point| O_X_p} 
9. q' : {p:Point| O_X_p} 
10. p' = c + a ∈ Length
11. q' = c + b ∈ Length
12. X_p'_q'
⊢ Ax ∈ a ≤ b

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  O\_X\_a
4.  b  :  Point
5.  O\_X\_b
6.  c  :  Point
7.  O\_X\_c
8.  c  +  a  \mleq{}  c  +  b
\mvdash{}  Ax  \mmember{}  a  \mleq{}  b


By

---

Latex:
(Unfold  `geo-le`  -1  THEN  SqExRepD)

---

Home Index