Problem (2014CHNSouthEastMOg11p1): Let $ABC$ be a triangle with $AB<AC$ and let $M $ be the midpoint of $BC$. $MI$ ($I$ incenter) intersects $AB$ at $D$ and $CI$ intersects the circumcircle of $ABC$ at $E$. Prove that $\frac{ED }{ EI} = \frac{IB }{IC}$
AlphaGeometry formalization: a b c = triangle; m = midpoint b c; i = incenter a b c; d = on_line a b, on_line m i; o = circumcenter a b c; e = on_line c i, on_circle o a ? eqratio e d e i i b i c
HAGeo formalization: A B C = triangle; M = midpoint B C; I = incenter A B C; IM = line I M; AB = line A B; D = intersection IM AB; CI = line C I; O = circumcenter A B C; (O) = circle_center_point O A; E = intersection CI (O); Prove: equal_ratio D E E I B I C I
Difficulty score: 2.2