theorem EuclidGeom.Shan_Problem_1_3.A_ne_B {P : Type u_1} {A : P} {B : P} : A ≠ B

theorem EuclidGeom.Shan_Problem_1_3.B_ne_C {P : Type u_1} {B : P} {C : P} : B ≠ C

theorem EuclidGeom.Shan_Problem_1_3.c_ne_a {P : Type u_1} {A : P} {C : P} : C ≠ A

theorem EuclidGeom.Shan_Problem_1_3.Shan_Problem_1_3 {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {D : P} {E : P} : { source := C, target := D }.length = 2 * { source := C, target := E }.length

theorem EuclidGeom.Shan_Problem_1_4.A_ne_B {P : Type u_1} {A : P} {B : P} : A ≠ B

theorem EuclidGeom.Shan_Problem_1_4.B_ne_C {P : Type u_1} {B : P} {C : P} : B ≠ C

theorem EuclidGeom.Shan_Problem_1_4.c_ne_a {P : Type u_1} {A : P} {C : P} : C ≠ A

theorem EuclidGeom.Shan_Problem_1_4.Shan_Problem_1_4 {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {D : P} : { source := B, target := D }.length = { source := A, target := C }.length + { source := C, target := D }.length