---

Step * of Lemma geo-add-length-cancel-left-lt

∀[e:BasicGeometry]. ∀[x,y,z:Length].  (z + x < z + y ⇒ x < y)
BY
{ (Auto THEN RepeatFor 4 (ParallelLast)) }

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

---

Latex:

---

Latex:
\mforall{}[e:BasicGeometry].  \mforall{}[x,y,z:Length].    (z  +  x  <  z  +  y  {}\mRightarrow{}  x  <  y)


By

---

Latex:
(Auto  THEN  RepeatFor  4  (ParallelLast))

---

Home Index