---

Step * of Lemma geo-le-add1

∀e:BasicGeometry. ∀[p,q:Length].  p ≤ p + q
BY
{ (Auto
   THEN UseWitness ⌜Ax⌝⋅
   THEN ∀h:hyp. (UnfoldTop `geo-length-type` h THEN (D h THENA Auto)) 
   THEN ((Fold `member` 0 THEN All (Unfold `geo-le`)) THEN SqExRepD)
   THEN ∀h:hyp. (Unfold `geo-length-type` h THEN (EqTypeHD h THENA Auto)) 
   THEN MemTypeCD
   THEN (Assert {p:Point| O_X_p}  ⊆r Length BY
               Auto)
   THEN InstConcl [⌜p⌝;⌜p + q⌝]⋅
   THEN Try (RepeatFor 2 (MemCD))
   THEN Auto) }

1
1. e : BasicGeometry
2. p : Base
3. p1 : Base
4. p = p1 ∈ (x,y:{p:Point| O_X_p} //x ≡ y)
5. p ∈ {p:Point| O_X_p} 
6. p1 ∈ {p:Point| O_X_p} 
7. p ≡ p1
8. q : Base
9. q1 : Base
10. q = q1 ∈ (x,y:{p:Point| O_X_p} //x ≡ y)
11. q ∈ {p:Point| O_X_p} 
12. q1 ∈ {p:Point| O_X_p} 
13. q ≡ q1
14. {p:Point| O_X_p}  ⊆r Length
15. p = p ∈ Length
16. p + q = p + q ∈ Length
⊢ X_p_p + q

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}[p,q:Length].    p  \mleq{}  p  +  q


By

---

Latex:
(Auto
  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
  THEN  \mforall{}h:hyp.  (UnfoldTop  `geo-length-type`  h  THEN  (D  h  THENA  Auto)) 
  THEN  ((Fold  `member`  0  THEN  All  (Unfold  `geo-le`))  THEN  SqExRepD)
  THEN  \mforall{}h:hyp.  (Unfold  `geo-length-type`  h  THEN  (EqTypeHD  h  THENA  Auto)) 
  THEN  MemTypeCD
  THEN  (Assert  \{p:Point|  O\_X\_p\}    \msubseteq{}r  Length  BY
                          Auto)
  THEN  InstConcl  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}p  +  q\mkleeneclose{}]\mcdot{}
  THEN  Try  (RepeatFor  2  (MemCD))
  THEN  Auto)

---

Home Index