Problem (2010AsiaPacificMOp1): Let $ABC$ be a triangle with $\angle BAC \neq 90^{\circ}.$ Let $O$ be the circumcenter of the triangle $ABC$ and $\Gamma$ be the circumcircle of the triangle $BOC.$ Suppose that $\Gamma$ intersects the line segment $AB$ at $P$ different from $B$, and the line segment $AC$ at $Q$ different from $C.$ Let $ON$ be the diameter of the circle $\Gamma.$ Prove that the quadrilateral $APNQ$ is a parallelogram.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; o1 = circumcenter o b c; p = on_line a b, on_circle o1 o; q = on_line a c, on_circle o1 o; n = mirror o o1 ? para a p n q
HAGeo formalization: A B C = triangle; O = circumcenter A B C; O1 = circumcenter O B C; (O1) = circle_center_point O1 O; AB = line A B; P = intersection AB (O1); AC = line A C; Q = intersection AC (O1); N = reflect_point_wrt_point O O1; AP = line A P; NQ = line N Q; Prove: parallel AP NQ
Difficulty score: 1.4