theorem EuclidGeom.Shan_Problem_1_9.a_ne_b {P : Type u_1} {A : P} {B : P} : A ≠ B

theorem EuclidGeom.Shan_Problem_1_9.b_ne_c {P : Type u_1} {B : P} {C : P} : B ≠ C

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

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

theorem EuclidGeom.Shan_Problem_1_10.a_ne_b {P : Type u_1} {A : P} {B : P} : A ≠ B

theorem EuclidGeom.Shan_Problem_1_10.b_ne_c {P : Type u_1} {B : P} {C : P} : B ≠ C

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

theorem EuclidGeom.Shan_Problem_1_10.Shan_Problem_1_10 {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {E : P} {he₁ : EuclidGeom.lies_int E (EuclidGeom.SegND.extension (SEG_nd A C (_ : C ≠ A)))} {he₂ : { source := A, target := E }.length = { source := B, target := C }.length} {D : P} : { source := A, target := D }.length = { source := D, target := C }.length