Problem (2000USATSTp2): Let $ ABCD$ be a cyclic quadrilateral and let $ E$ and $ F$ be the feet of perpendiculars from the intersection of diagonals $ AC$ and $ BD$ to $ AB$ and $ CD$, respectively. Prove that $ EF$ is perpendicular to the line through the midpoints of $ AD$ and $ BC$.
AlphaGeometry formalization: a b c = triangle; d = on_circum a b c; p = on_line a c, on_line b d; e = foot p a b; f = foot p c d; m = midpoint a d; n = midpoint b c ? perp e f m n
HAGeo formalization: A B C = triangle; (ABC) = circle A B C; D = on_circle (ABC); AC = line A C; BD = line B D; P = intersection AC BD; AB = line A B; E = foot P AB; CD = line C D; F = foot P CD; M = midpoint A D; N = midpoint B C; EF = line E F; MN = line M N; Prove: perpendicular EF MN
Difficulty score: 2.3