Cauchy–Schwarz

Finally I understand the Cauchy–Schwarz inequality! No induction needed.

Theorem
$a, b\in \mathrm{Rat}^n$
$n\in\mathrm{Nat}$
                     
$(a\bullet b)^2 \leq \mathop{\rm Q}(a)\mathop{\rm Q}(b)$

Proof
Recall that by definition
$$a\bullet b=\sum_{i=1}^n a_ib_i$$ $$\mathop{\rm Q}(a)=\sum_{i=1}^n a_i^2$$ $$\mathop{\rm Q}(b)=\sum_{i=1}^n b_i^2.$$
The claim, reformulated as
$$\left(\sum_{i=1}^n a_ib_i\right)^2 \leq \left(\sum_{i=1}^n a_i^2\right)\left(\sum_{i=1}^n b_i^2\right),$$
is equivalent to (by distributing terms)
$$\left(\sum_{i=1}^n a_i^2b_i^2\right)+\sum_{1\leq i<j\leq n}2a_ib_ia_jb_j \leq \left(\sum_{i=1}^n a_i^2b_i^2\right)+\sum_{1\leq i<j\leq n}a_i^2b_j^2+a_j^2b_i^2$$
and (by collecting terms)
$$0 \leq \sum_{1\leq i<j\leq n}a_i^2b_j^2+a_j^2b_i^2-2a_ib_ia_jb_j = \sum_{1\leq i<j\leq n}(a_ib_j-a_jb_i)^2.$$
The last statement is true because squares are positive and sums of positive numbers are positive.