Constructive proof of the Cauchy Schwarz inequality The famous CS inequality states

$$
\left| \left&lt; x , y \right&gt;\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 &gt; 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 }$.
I don't think that you can actually prove Cauchy-Schwartz (CS) for an arbitrary inner product space (constructively). In Constructive Analysis by Bishop &amp; 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:
Breaking into cases doesn't necessarily rely on the law of excluded middle. It is true in a Hilbert space that either $x = 0$ or $x \neq 0$, we don't need to appeal to excluded middle for this fact. This constructively/intuitionistically reduces the problem to finding a proof for both the case $x=0$ and the case $x \neq 0$.

In other words, I agree that a case analysis uses excluded middle in some sense, but if you can constructively prove excluded middle for the cases you are considering, then you don't need to assume it in general.