---

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

∀e:BasicGeometry. ∀y,z:Length.  (z < z + y ⇐⇒ 0 < y)
BY
{ Auto }

1
1. e : BasicGeometry
2. y : Length
3. z : Length
4. z < z + y
⊢ 0 < y

2
1. e : BasicGeometry
2. y : Length
3. z : Length
4. 0 < y
⊢ z < z + y

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}y,z:Length.    (z  <  z  +  y  \mLeftarrow{}{}\mRightarrow{}  0  <  y)


By

---

Latex:
Auto

---

Home Index