---

Step * 2 of Lemma geo-same-side-iff


1. e : BasicGeometry
2. A : Point
3. B : Point
4. P : Point
5. Q : Point
6. P,Q-AB
7. ¬Q leftof AB
⊢ ¬P leftof AB
BY
{ ((D 0 THENA Auto)
   THEN Unfold `geo-same-side` -3
   THEN ((StableCases ⌜Q # BA⌝⋅ THENA Auto)
   THENL [ (D -1 THEN Auto);((RWO "not-lsep-iff-colinear" (-1) THENA Auto) THEN InstHyp [⌜Q⌝] 6⋅ THEN Auto)⋅])) }

1
1. e : BasicGeometry
2. A : Point
3. B : Point
4. P : Point
5. Q : Point
6. ∀T:Point. (P_T_Q ⇒ (¬Colinear(A;B;T)))
7. ¬Q leftof AB
8. P leftof AB
9. Q leftof BA
⊢ False

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  A  :  Point
3.  B  :  Point
4.  P  :  Point
5.  Q  :  Point
6.  P,Q-AB
7.  \mneg{}Q  leftof  AB
\mvdash{}  \mneg{}P  leftof  AB


By

---

Latex:
((D  0  THENA  Auto)
  THEN  Unfold  `geo-same-side`  -3
  THEN  ((StableCases  \mkleeneopen{}Q  \#  BA\mkleeneclose{}\mcdot{}  THENA  Auto)
  THENL  [  (D  -1  THEN  Auto);((RWO  "not-lsep-iff-colinear"  (-1)  THENA  Auto)
                                                      THEN  InstHyp  [\mkleeneopen{}Q\mkleeneclose{}]  6\mcdot{}
                                                      THEN  Auto)\mcdot{}]))

---

Home Index