---

Step * of Lemma geo-add-length-le-implies-eq

∀[e:BasicGeometry]. ∀[x:Length]. ∀[a,b:Point].  a ≡ b supposing x + |ab| ≤ x
BY
{ (Auto THEN (Assert x + |ab| ≤ x + 0 BY (Unfold `geo-zero-length` 0 THEN RWO "geo-add-length-zero" 0 THEN Auto))) }

1
1. e : BasicGeometry
2. x : Length
3. a : Point
4. b : Point
5. x + |ab| ≤ x
6. x + |ab| ≤ x + 0
⊢ a ≡ b

---

Latex:

---

Latex:
\mforall{}[e:BasicGeometry].  \mforall{}[x:Length].  \mforall{}[a,b:Point].    a  \mequiv{}  b  supposing  x  +  |ab|  \mleq{}  x


By

---

Latex:
(Auto
  THEN  (Assert  x  +  |ab|  \mleq{}  x  +  0  BY
                          (Unfold  `geo-zero-length`  0  THEN  RWO  "geo-add-length-zero"  0  THEN  Auto))
  )

---

Home Index