---

Step * of Lemma bnot-isleft

∀g:OrientedPlane. ∀a,b:Point. ∀c:{c:Point| a # bc} .  ¬bisleft(a;b;c) = isleft(a;c;b)
BY
{ (Auto THEN ((BLemma `iff_imp_equal_bool` THENM RW assert_pushdownC 0) THENA Auto)) }

1
1. g : OrientedPlane
2. a : Point
3. b : Point
4. c : {c:Point| a # bc} 
⊢ ¬a leftof bc ⇐⇒ a leftof cb

---

Latex:

---

Latex:
\mforall{}g:OrientedPlane.  \mforall{}a,b:Point.  \mforall{}c:\{c:Point|  a  \#  bc\}  .    \mneg{}\msubb{}isleft(a;b;c)  =  isleft(a;c;b)


By

---

Latex:
(Auto  THEN  ((BLemma  `iff\_imp\_equal\_bool`  THENM  RW  assert\_pushdownC  0)  THENA  Auto))

---

Home Index