theorem EuclidGeom.pt_flip_center_is_midpoint {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {O : P} (h : B = EuclidGeom.pt_flip A O) : O = { source := A, target := B }.midpoint