Lean-Workbook Plus 26955: Trigonometric identity

For every natural number $n$ and real $x$, $\sin^2(nx)=\tfrac12(1-\cos(2nx))$.

Source: Lean-Workbook row lean_workbook_plus_26955 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.