Problem (2016SilkRoadp2): Around the acute-angled triangle $ABC$ ($AC>CB$) a circle is circumscribed, and the point $N$ is midpoint of the arc $ACB$ of this circle. Let the points $A_1$ and $B_1$ be the feet of perpendiculars on the straight line $NC$, drawn from points $A$ and $B$ respectively (segment $NC$ lies inside the segment $A_1B_1$). Altitude $A_1A_2$ of triangle $A_1AC$ and altitude $B_1B_2$ of triangle $B_1BC$ intersect at a point $K$ . Prove that $\angle A_1KN=\angle B_1KM$, where $M$ is midpoint of the segment $A_2B_2$ .
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; n = on_bline a b, on_circum a b c; a1 = foot a n c; b1 = foot b n c; a2 = foot a1 a c; b2 = foot b1 b c; k = on_line a1 a2, on_line b1 b2; m = midpoint a2 b2 ? eqangle a1 k k n k m b1 k
HAGeo formalization: A B C = acute_triangle; N = midarc A C B; CN = line C N; A1 = foot A CN; B1 = foot B CN; AC = line A C; A2 = foot A1 AC; BC = line B C; B2 = foot B1 BC; A1A2 = line A1 A2; B1B2 = line B1 B2; K = intersection A1A2 B1B2; M = midpoint A2 B2; Prove: equal_angle A1 K N M K B1
Difficulty score: 2.5