---

Step * 1 1 of Lemma geo-zero-lt-iff


1. e : BasicGeometry
2. u : Point
3. v : Point
4. ∀[x:Length]. (x + 0 = x ∈ Length)
5. a : Point
6. b : Point
7. a ≠ b
8. |ab| ≤ |uv|
⊢ u ≠ v
BY
{ ((RWO "geo-le-iff" (-1) THENA Auto) THEN FLemma `geo-ge-sep` [-1] THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  u  :  Point
3.  v  :  Point
4.  \mforall{}[x:Length].  (x  +  0  =  x)
5.  a  :  Point
6.  b  :  Point
7.  a  \mneq{}  b
8.  |ab|  \mleq{}  |uv|
\mvdash{}  u  \mneq{}  v


By

---

Latex:
((RWO  "geo-le-iff"  (-1)  THENA  Auto)  THEN  FLemma  `geo-ge-sep`  [-1]  THEN  Auto)

---

Home Index