theorem
EuclidGeom.pts_are_distinct_of_two_rays_of_angle
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
(ang : EuclidGeom.Angle P)
(nontriv : ang.IsND)
(A : P)
(B : P)
(ha : EuclidGeom.lies_int A ang.start_ray)
(hb : EuclidGeom.lies_int B ang.end_ray)
:
A ≠ B
theorem
EuclidGeom.Ray.left_iff_not_right_of_not_lies_on
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{a : P}
{l : EuclidGeom.Ray P}
(h : ¬EuclidGeom.lies_on a l)
:
theorem
EuclidGeom.Ray.not_lies_on_iff_left_or_right
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
(a : P)
(l : EuclidGeom.Ray P)
: