Problem (2020IOMetrop1): In a triangle $ABC$ with a right angle at $C$, the angle bisector $AL$ (where $L$ is on segment $BC$) intersects the altitude $CH$ at point $K$. The bisector of angle $BCH$ intersects segment $AB$ at point $M$. Prove that $CK=ML$
AlphaGeometry formalization: c a b = r_triangle; l = on_line b c, angle_bisector b a c; h = foot c a b; k = on_line c h, angle_bisector b a c; m = on_line a b, angle_bisector b c h ? cong c k m l
HAGeo formalization: C A B = right_triangle; l1 = angle_bisector B A C; BC = line B C; L = intersection l1 BC; AB = line A B; H = foot C AB; AL = line A L; CH = line C H; K = intersection AL CH; l2 = angle_bisector B C H; M = intersection l2 AB; Prove: cong C K M L
Difficulty score: 1.4