The famous CS inequality states
$$
\left| \left< x , y \right>\right|
\le \left\| x \right\| \cdot \left\| y \right\|
$$
for $x,y$ in an inner product space $X$ over $\mathbb{K}$. Every proof I found involves some kind of case distinction; namely one may use w.l.o.g $\Vert x \Vert, \Vert y \Vert > 0$ since the inequality is trivial otherwise. However, I was looking for a constructive proof (i.e. without using the law of excluded middle) for the inequality.
I will add some remarks to the question.
1) Law of excluded middle: This axiom states that $A \vee \neg A$ is true. This is not considered an axiom in constructive mathematics. One might interpret this in the following way: Indirect proofs are not allowed. However, I find this not completely accurate. Precisely the implication $A \rightarrow \neg \neg A$ is true in constructive mathematics; the implication $ \neg \neg A \rightarrow A$ not in gerneral.
2) The definition of an inner product is the same as in "classical" mathematics.
3) The norm $\Vert \cdot \Vert$ is given by $\Vert x \Vert = \sqrt{\langle x, x\rangle }$.
Best Answer
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: