theorem EuclidGeom.wedge_add_wedge_eq_wedge_add_wedge {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (D : P) : EuclidGeom.wedge A B C + EuclidGeom.wedge C D A = EuclidGeom.wedge B C D + EuclidGeom.wedge D A B

theorem EuclidGeom.wedge_eq_wedge_add_wedge_of_collinear {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (D : P) (colin : EuclidGeom.Collinear A B C) : EuclidGeom.wedge D A C = EuclidGeom.wedge D B C + EuclidGeom.wedge D A B

theorem EuclidGeom.wedge_eq_divratio_mul_wedge_of_collinear {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (D : P) (colin : EuclidGeom.Collinear A B C) [cnea : EuclidGeom.PtNe C A] : EuclidGeom.wedge A B D = EuclidGeom.divratio A B C * EuclidGeom.wedge A C D

theorem EuclidGeom.odist_eq_divratio_mul_odist {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (dl : EuclidGeom.DirLine P) (colin : EuclidGeom.Collinear A B C) [cnea : EuclidGeom.PtNe C A] (aisondl : EuclidGeom.lies_on A dl) : EuclidGeom.odist B dl = EuclidGeom.divratio A B C * EuclidGeom.odist C dl

theorem EuclidGeom.wedge_eq_divratio_mul_wedge_of_collinear_collinear {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (D : P) (E : P) (colin : EuclidGeom.Collinear A B C) [cnea : EuclidGeom.PtNe C A] (colin' : EuclidGeom.Collinear A D E) : EuclidGeom.wedge D B E = EuclidGeom.divratio A B C * EuclidGeom.wedge D C E

theorem EuclidGeom.ratio_eq_wedge_div_wedge_of_collinear_collinear_notcoliear {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (D : P) (E : P) (colin : EuclidGeom.Collinear A B C) [cnea : EuclidGeom.PtNe C A] (colin' : EuclidGeom.Collinear A D E) (ncolin : ¬EuclidGeom.Collinear D C E) : EuclidGeom.divratio A B C = EuclidGeom.wedge D B E / EuclidGeom.wedge D C E