Problem (2014CHNSouthEastMOg10p3): In an obtuse triangle $ABC$ $(AB>AC)$,$O$ is the circumcentre and $D,E,F$ are the midpoints of $BC,CA,AB$ respectively.Median $AD$ intersects $OF$ and $OE$ at $M$ and $N$ respectively.$BM$ meets $CN$ at point $P$.Prove that
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; d = midpoint b c; e = midpoint c a; f = midpoint a b; m = on_line a d, on_line o f; n = on_line a d, on_line o e; p = on_line b m, on_line c n ? perp a p o p
HAGeo formalization: A B C = obtuse_triangle; O = circumcenter A B C; D = midpoint B C; E = midpoint C A; F = midpoint A B; AD = line A D; FO = line F O; M = intersection AD FO; EO = line E O; N = intersection AD EO; BM = line B M; CN = line C N; P = intersection BM CN; OP = line O P; AP = line A P; Prove: perpendicular OP AP
Difficulty score: 3.6