Problem (2018CHNWesternMOp5): In acute triangle $ABC,$ $AB<AC,$ $O$ is the circumcenter of the triangle. $M$ is the midpoint of segment $BC,$ $(AOM)$ intersects the line $AB$ again at $D$ and intersects the segment $AC$ at $E.$ Prove that $DM=EC.$
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; m = midpoint b c; o1 = circumcenter a o m; d = on_line a b, on_circle o1 a; e = on_line a c, on_circle o1 a ? cong d m e c
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; M = midpoint B C; O1 = circumcenter A O M; (O1) = circle A M O; AB = line A B; D = intersection (O1) AB; AC = line A C; E = intersection (O1) AC; Prove: cong D M E C
Difficulty score: 1.4