---

Step * 2 of Lemma geo-seg-congruent-iff-length


1. e : BasicGeometry
2. s : geo-segment(e)
3. t : geo-segment(e)
4. |s| ≡ |t|
⊢ geo-seg-congruent(e; s; t)
BY
{ (Unfold `geo-length` -1 THEN Unfold `geo-seg-congruent` 0 THEN RWO "geo-extend-equal-iff-congruent" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  s  :  geo-segment(e)
3.  t  :  geo-segment(e)
4.  |s|  \mequiv{}  |t|
\mvdash{}  geo-seg-congruent(e;  s;  t)


By

---

Latex:
(Unfold  `geo-length`  -1
  THEN  Unfold  `geo-seg-congruent`  0
  THEN  RWO  "geo-extend-equal-iff-congruent"  (-1)
  THEN  Auto)

---

Home Index