Constructive proof of the Cauchy Schwarz inequality

I don't think that you can actually prove Cauchy-Schwartz (CS) for an arbitrary inner product space (constructively). In Constructive Analysis by Bishop & Bridges they define inner product spaces so that CS holds:

However, for the special case of $\mathbb{R}^n$ it is possible to give a constructive proof, which can be found on page 83 of Constructive Analysis: