theorem
EuclidGeom.liesonleft_iff_liesonright_reverse
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{l : EuclidGeom.DirLine P}
:
EuclidGeom.IsOnLeftSide A l ↔ EuclidGeom.IsOnRightSide A l.reverse
theorem
EuclidGeom.DirLine.lieson_or_liesonleft_or_liesonright
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
(A : P)
(l : EuclidGeom.DirLine P)
:
theorem
EuclidGeom.eq_toDir_of_parallel_and_IsOnLL
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
{D : P}
[bnea : EuclidGeom.PtNe B A]
[cnea : EuclidGeom.PtNe C A]
[dneb : EuclidGeom.PtNe D B]
(para : EuclidGeom.Parallel (SEG_nd A C) (SEG_nd B D))
(side : EuclidGeom.IsOnLeftSide C (SEG_nd A B) ∧ EuclidGeom.IsOnLeftSide D (SEG_nd A B))
:
(SEG_nd A C).toDir = (SEG_nd B D).toDir
theorem
EuclidGeom.eq_toDir_of_parallel_and_IsOnRR
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
{D : P}
[bnea : EuclidGeom.PtNe B A]
[cnea : EuclidGeom.PtNe C A]
[dneb : EuclidGeom.PtNe D B]
(para : EuclidGeom.Parallel (SEG_nd A C) (SEG_nd B D))
(side : EuclidGeom.IsOnRightSide C (SEG_nd A B) ∧ EuclidGeom.IsOnRightSide D (SEG_nd A B))
:
(SEG_nd A C).toDir = (SEG_nd B D).toDir
theorem
EuclidGeom.eq_toDir_of_parallel_and_IsOnSameSide
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
{D : P}
[bnea : EuclidGeom.PtNe B A]
[cnea : EuclidGeom.PtNe C A]
[dneb : EuclidGeom.PtNe D B]
(para : EuclidGeom.Parallel (SEG_nd A C) (SEG_nd B D))
(side : EuclidGeom.IsOnSameSide C D (SEG_nd A B))
:
(SEG_nd A C).toDir = (SEG_nd B D).toDir
theorem
EuclidGeom.neg_toDir_of_parallel_and_IsOnLR
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
{D : P}
[bnea : EuclidGeom.PtNe B A]
[cnea : EuclidGeom.PtNe C A]
[dneb : EuclidGeom.PtNe D B]
(para : EuclidGeom.Parallel (SEG_nd A C) (SEG_nd B D))
(side : EuclidGeom.IsOnLeftSide C (SEG_nd A B) ∧ EuclidGeom.IsOnRightSide D (SEG_nd A B))
:
theorem
EuclidGeom.neg_toDir_of_parallel_and_IsOnRL
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
{D : P}
[bnea : EuclidGeom.PtNe B A]
[cnea : EuclidGeom.PtNe C A]
[dneb : EuclidGeom.PtNe D B]
(para : EuclidGeom.Parallel (SEG_nd A C) (SEG_nd B D))
(side : EuclidGeom.IsOnRightSide C (SEG_nd A B) ∧ EuclidGeom.IsOnLeftSide D (SEG_nd A B))
:
theorem
EuclidGeom.neg_toDir_of_parallel_and_IsOnOppositeSide
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
{D : P}
[bnea : EuclidGeom.PtNe B A]
[cnea : EuclidGeom.PtNe C A]
[dneb : EuclidGeom.PtNe D B]
(para : EuclidGeom.Parallel (SEG_nd A C) (SEG_nd B D))
(side : EuclidGeom.IsOnOppositeSide C D (SEG_nd A B))
: