Problem (2016CTSTp5): Refer to the diagram below. Let $ABCD$ be a cyclic quadrilateral with center $O$. Let the internal angle bisectors of $\angle A$ and $\angle C$ intersect at $I$ and let those of $\angle B$ and $\angle D$ intersect at $J$. Now extend $AB$ and $CD$ to intersect $IJ$ and $P$ and $R$ respectively and let $IJ$ intersect $BC$ and $DA$ at $Q$ and $S$ respectively. Let the midpoints of $PR$ and $QS$ be $M$ and $N$ respectively. Given that $O$ does not lie on the line $IJ$, show that $OM$ and $ON$ are perpendicular.
AlphaGeometry formalization: a b c = triangle; d = on_circum a b c; o = circumcenter a b c; i = angle_bisector d a b, angle_bisector b c d; j = angle_bisector a b c, angle_bisector c d a; p = on_line a b, on_line i j; r = on_line c d, on_line i j; q = on_line b c, on_line i j; s = on_line d a, on_line i j; m = midpoint p r; n = midpoint q s ? perp o m o n
HAGeo formalization: A B C = triangle; (ABC) = circle A B C; D = on_circle (ABC); O = circumcenter A B C; l1 = angle_bisector B A D; l2 = angle_bisector B C D; I = intersection l1 l2; l3 = angle_bisector A B C; l4 = angle_bisector C D A; J = intersection l3 l4; AB = line A B; IJ = line I J; P = intersection AB IJ; CD = line C D; R = intersection CD IJ; BC = line B C; Q = intersection IJ BC; AD = line A D; S = intersection IJ AD; M = midpoint P R; N = midpoint Q S; MO = line M O; NO = line N O; Prove: perpendicular MO NO
Difficulty score: 4.3