theorem
EuclidGeom.Exercise_3_4_4.A_ne_B
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
{hnd : ¬EuclidGeom.Collinear A B C}
:
A ≠ B
theorem
EuclidGeom.Exercise_3_4_4.A_ne_C
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
{hnd : ¬EuclidGeom.Collinear A B C}
:
A ≠ C
theorem
EuclidGeom.Exercise_3_4_4.x_ne_B
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
{hnd : ¬EuclidGeom.Collinear A B C}
{X : P}
{hx : EuclidGeom.lies_int X { source := A, target := C }}
:
X ≠ B
theorem
EuclidGeom.Exercise_3_4_4.y_ne_C
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
{hnd : ¬EuclidGeom.Collinear A B C}
{Y : P}
{hy : EuclidGeom.lies_int Y { source := A, target := B }}
:
Y ≠ C