Problem (2011CHNSouthEastMOp4): Let $O$ be the circumcenter of triangle $ABC$ , a line passes through $O$ intersects sides $AB,AC$ at points $M,N$ , $E$ is the midpoint of $MC$ , $F$ is the midpoint of $NB$ , prove that : $\angle FOE= \angle BAC$
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; m = on_line a b; n = on_line a c, on_line o m; e = midpoint n b; f = midpoint m c ? eqangle f o o e c a a b
HAGeo formalization: A B C = triangle; O = circumcenter A B C; AB = line A B; M = on_line AB; AC = line A C; OM = line O M; N = intersection OM AC; E = midpoint M C; F = midpoint N B; Prove: equal_angle F O E B A C
Difficulty score: 3.4