Solution (source code)

= Solution

<Cauchy-Schwarz inequality> states $|x\cdot y|\le\|x\|\|y\|$. For $y\ne0$, positivity of $\|x-ty\|^2$ at $t=(x\cdot y)/\|y\|^2$ gives $\|x\|^2-(x\cdot y)^2/\|y\|^2\ge0$; $y=0$ is immediate.