Rewriting a quotient using two zero sums

Let $x_1+x_2+x_3= 0 \implies x_1x_2= \frac{x_3^2-x_1^2-x_2^2}{2}$ $y_1+y_2+y_3= 0 \implies y_1y_2= \frac{y_3^2-y_1^2-y_2^2}{2}$ $\frac{x_1x_2+y_1y_2}{\sqrt{(x_1^2+y_1^2)(x_2^2+y_2^2)}}=-\frac{(x_1^2+y_1^2)+(x_2^2+y_2^2)-(x_3^2+y_3^2)}{2\sqrt{(x_1^2+y_1^2)(x_2^2+y_2^2)}}$

Source: InternLM Lean-Workbook, record lean_workbook_22885 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.