Problem (2013CHNGaoLianA): $AB$ is a chord of circle $\omega$, $P$ is a point on minor arc $AB$, $E,F$ are on segment $AB$ such that $AE=EF=FB$. $PE,PF$ meets $\omega$ at $C,D$ respectively. Prove that $EF\cdot CD=AC\cdot BD$.
AlphaGeometry formalization: a b = segment; o = on_bline a b; p = on_circle o a; e f = trisegment a b; c = on_line p e, on_circle o a; d = on_line p f, on_circle o a ? eqratio e f a c b d c d
HAGeo formalization: A = point; B = point; l = perpendicular_bisector A B; O = on_line l; (O) = circle_center_point O A; P = on_circle (O); E F = trisegment A B; EP = line E P; C = intersection EP (O); FP = line F P; D = intersection FP (O); Prove: equal_ratio E F A C B D C D
Difficulty score: 2.0