---

Step * 2 of Lemma geo-lt-add1-iff


1. e : BasicGeometry
2. p : {a:Point| O_X_a} 
3. q : {a:Point| O_X_a} 
4. r : {a:Point| O_X_a} 
5. X ≠ p
6. X ≠ q
7. X ≠ r
8. p + r < q + r
⊢ p < q
BY
{ (((Assert p + r = r + p ∈ Length BY Auto) THEN (Assert q + r = r + q ∈ Length BY Auto))
   THEN InstLemma `geo-add-length-cancel-left-lt` [⌜e⌝;⌜p⌝;⌜q⌝;⌜r⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  p  :  \{a:Point|  O\_X\_a\} 
3.  q  :  \{a:Point|  O\_X\_a\} 
4.  r  :  \{a:Point|  O\_X\_a\} 
5.  X  \mneq{}  p
6.  X  \mneq{}  q
7.  X  \mneq{}  r
8.  p  +  r  <  q  +  r
\mvdash{}  p  <  q


By

---

Latex:
(((Assert  p  +  r  =  r  +  p  BY  Auto)  THEN  (Assert  q  +  r  =  r  +  q  BY  Auto))
  THEN  InstLemma  `geo-add-length-cancel-left-lt`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index