---

Step * 1 of Lemma not-geo-lt


1. g : EuclideanPlane
2. p : Length
3. q : Length
4. ¬p < q
⊢ q ≤ p
BY
{ ((StableCases ⌜q ≤ p⌝⋅ THEN Auto) THEN Assert ⌜False⌝⋅ THEN Auto) }

1
.....assertion..... 
1. g : EuclideanPlane
2. p : Length
3. q : Length
4. ¬p < q
5. ¬q ≤ p
⊢ False

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  p  :  Length
3.  q  :  Length
4.  \mneg{}p  <  q
\mvdash{}  q  \mleq{}  p


By

---

Latex:
((StableCases  \mkleeneopen{}q  \mleq{}  p\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index