---

Step * of Lemma geo-add-length_functionality_wrt_lt

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

1
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' + y'

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  RepeatFor  4  (ParallelLast))

---

Home Index