---

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


1. e : BasicGeometry
2. A : Point
3. B : Point
4. P : Point
5. Q : Point
6. P-AB-Q
7. ¬Q leftof BA
⊢ ¬P leftof AB
BY
{ ((D 0 THENA Auto)
   THEN Unfold `geo-opp-side` -3
   THEN Auto
   THEN (StableCases ⌜Q # AB⌝⋅ THENA Auto)
   THEN (((RWO "not-lsep-iff-colinear" (-1) THENA Auto) THEN D 8 THEN Auto) ORELSE (D -1 THEN Try (Trivial)))) }

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. ¬Colinear(A;B;P)
8. ¬Colinear(A;B;Q)
9. ¬Q leftof BA
10. P leftof AB
11. Q leftof AB
⊢ False

---

Latex:

---

Latex:

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


By

---

Latex:
((D  0  THENA  Auto)
  THEN  Unfold  `geo-opp-side`  -3
  THEN  Auto
  THEN  (StableCases  \mkleeneopen{}Q  \#  AB\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (((RWO  "not-lsep-iff-colinear"  (-1)  THENA  Auto)  THEN  D  8  THEN  Auto)
  ORELSE  (D  -1  THEN  Try  (Trivial))
  ))

---

Home Index