theorem EuclidGeom.pt_flip_collinear {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {O : P} (h : B = EuclidGeom.pt_flip A O) : EuclidGeom.Collinear A O B

theorem EuclidGeom.exist_dirline_of_line {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.Line P) : ∃ (Dl : EuclidGeom.DirLine P), Dl.toLine = l