---

Step * of Lemma geo-gt-implies-lt

∀g:EuclideanPlane. ∀a,b,c,d:Point.  (ab > cd ⇒ (¬¬|cd| < |ab|))
BY
{ ((((((Auto THEN D -1 THEN Auto) THEN ExRepD) THEN RemoveDoubleNegation) THEN Auto)
    THEN Unfold `geo-lt` 0
    THEN InstConcl [⌜w⌝;⌜b⌝]⋅
    THEN Auto)
   THEN (FLemma `geo-add-length-between` [7] THENA Auto)
   THEN (Subst' |aw| + |wb| = |cd| + |wb| ∈ Length -1 THEN Auto)
   THEN RWO "-1" 0
   THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,d:Point.    (ab  >  cd  {}\mRightarrow{}  (\mneg{}\mneg{}|cd|  <  |ab|))


By

---

Latex:
((((((Auto  THEN  D  -1  THEN  Auto)  THEN  ExRepD)  THEN  RemoveDoubleNegation)  THEN  Auto)
    THEN  Unfold  `geo-lt`  0
    THEN  InstConcl  [\mkleeneopen{}w\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
    THEN  Auto)
  THEN  (FLemma  `geo-add-length-between`  [7]  THENA  Auto)
  THEN  (Subst'  |aw|  +  |wb|  =  |cd|  +  |wb|  -1  THEN  Auto)
  THEN  RWO  "-1"  0
  THEN  EAuto  1)

---

Home Index