Problem (2013ARMOg9p2): Acute-angled triangle $ABC$ is inscribed into circle $\Omega$. Lines tangent to $\Omega$ at $B$ and $C$ intersect at $P$. Points $D$ and $E$ are on $AB$ and $AC$ such that $PD$ and $PE$ are perpendicular to $AB$ and $AC$ respectively. Prove that the orthocentre of triangle $ADE$ is the midpoint of $BC$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; p = on_tline b o b, on_tline c o c; d = foot p a b; e = foot p a c; h = orthocenter a d e ? midp h b c
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; OB = line O B; OC = line O C; l1 = perpendicular_line B OB; l2 = perpendicular_line C OC; P = intersection l1 l2; AB = line A B; D = foot P AB; AC = line A C; E = foot P AC; H = orthocenter A D E; Prove: midpoint H B C
Difficulty score: 1.5