---

Step * 2 of Lemma geo-lt-add1-iff2


1. e : BasicGeometry
2. a1 : Point
3. a2 : Point
4. b1 : Point
5. b2 : Point
6. c1 : Point
7. c2 : Point
8. |a1a2| + |c1c2| < |b1b2| + |c1c2|
⊢ |a1a2| < |b1b2|
BY
{ (FLemma  `geo-add-length-cancel-right-lt` [8] THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a1  :  Point
3.  a2  :  Point
4.  b1  :  Point
5.  b2  :  Point
6.  c1  :  Point
7.  c2  :  Point
8.  |a1a2|  +  |c1c2|  <  |b1b2|  +  |c1c2|
\mvdash{}  |a1a2|  <  |b1b2|


By

---

Latex:
(FLemma    `geo-add-length-cancel-right-lt`  [8]  THEN  Auto)

---

Home Index