Problem (2002CTSTp25): Let $E$ and $F$ be the intersections of opposite sides of a convex quadrilateral $ABCD$. The two diagonals meet at $P$. Let $O$ be the foot of the perpendicular from $P$ to $EF$. Show that $\angle BOC=\angle AOD$.
AlphaGeometry formalization: a b c d = quadrangle; e = on_line a b, on_line c d; f = on_line a d, on_line b c; p = on_line a c, on_line b d; o = foot p e f ? eqangle b o o c a o o d
HAGeo formalization: A B C D = quadrilateral; AB = line A B; CD = line C D; E = intersection AB CD; AD = line A D; BC = line B C; F = intersection AD BC; AC = line A C; BD = line B D; P = intersection AC BD; EF = line E F; O = foot P EF; Prove: equal_angle B O C A O D
Difficulty score: 2.5