コーシー・シュワルツの不等式：\(\left(\sum a_i b_i\right)^2 \le \left(\sum a_i^2\right)\left(\sum b_i^2\right)\)。ここでは自然数の列 \(a, b\)（引き算の無い \(\mathbb{M}\) の上）で示す。不等式 \(x \le y\) は「\(y = x + t\) となる \(t \in \mathbb{M}\) がある」なので、\(n\) についての帰納法で余り \(t\) を運ぶ。
和は \(f\ \mathrm{sum}\ n\)（第 0 項から第 \(n-1\) 項まで）。

1 準備

2つの数の和の平方は、積の4倍より大きい：\((X+Y)^2 = 4XY + e\)。
Aam … \(X , Y \in \mathbb{M} \Longrightarrow \exists e \in \mathbb{M} . ( X + Y ) \cdot ( X + Y ) = 2 \cdot ( 2 \cdot ( X \cdot Y ) ) + e\) \(\blacktriangleleft\) Sx ，\(\mathbb{W}.\) ，Ax+𝕄 ，⋅𝕄 ，ℙ.'
平方が 0 なら 0。
Lkk … \(k \in \mathbb{M} , k \cdot k = 0 \Longrightarrow k = 0\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+𝕄 ，⋅𝕄
平方の大小から数の大小：\(z^2 + t = w^2\) なら \(w = z + s\)（\(s \in \mathbb{M}\)）。
Amono … \(z , w , t \in \mathbb{M} , z \cdot z + t = w \cdot w \Longrightarrow \exists s \in \mathbb{M} . w = z + s\) \(\blacktriangleleft\) Lkk ，Sx ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄 ，⋅𝕄 ，ℙ.'

2 帰納法の1歩

\(QR = P^2 + t\) なら \((Q + a^2)(R + b^2) = (P + ab)^2 + t'\)。\(X = Qb^2\)、\(Y = Ra^2\)、\(W = Pab\) とすると \(XY = W^2 + t a^2 b^2\)。\((X + Y)^2 \ge 4XY \ge (2W)^2\) から \(X + Y \ge 2W\)。
Mstep … \(P , Q , R , a , b , t \in \mathbb{M} , Q \cdot R = P \cdot P + t \Longrightarrow \exists t' \in \mathbb{M} . ( Q + a \cdot a ) \cdot ( R + b \cdot b ) = ( P + a \cdot b ) \cdot ( P + a \cdot b ) + t'\) \(\blacktriangleleft\) Aam ，Amono ，Sx ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄 ，⋅𝕄 ，ℙ.'

3 不等式

数列 \(a, b\) と、\(p_i = a_i b_i\)、\(q_i = a_i^2\)、\(r_i = b_i^2\) の和について、\(\left(\sum p\right)^2 + t = \left(\sum q\right)\left(\sum r\right)\) となる \(t\) がある。底と歩み。
LB … \(\forall i \in \mathbb{M} . a ( i ) \in \mathbb{M} , b ( i ) \in \mathbb{M} , p ( i ) = a ( i ) \cdot b ( i ) , q ( i ) = a ( i ) \cdot a ( i ) , r ( i ) = b ( i ) \cdot b ( i ) \Longrightarrow \exists t \in \mathbb{M} . ( q \sum 0 ) \cdot ( r \sum 0 ) = ( p \sum 0 ) \cdot ( p \sum 0 ) + t\) \(\blacktriangleleft\) Mstep ，Sx ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄 ，⋅𝕄 ，ℙ.' ，sum𝕄
LS … \(\forall i \in \mathbb{M} . a ( i ) \in \mathbb{M} , b ( i ) \in \mathbb{M} , p ( i ) = a ( i ) \cdot b ( i ) , q ( i ) = a ( i ) \cdot a ( i ) , r ( i ) = b ( i ) \cdot b ( i ) , n \in \mathbb{M} , \exists t \in \mathbb{M} . ( q \sum n ) \cdot ( r \sum n ) = ( p \sum n ) \cdot ( p \sum n ) + t \Longrightarrow \exists t \in \mathbb{M} . ( q \sum ( n + 1 ) ) \cdot ( r \sum ( n + 1 ) ) = ( p \sum ( n + 1 ) ) \cdot ( p \sum ( n + 1 ) ) + t\) \(\blacktriangleleft\) Mstep ，Sx ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄 ，⋅𝕄 ，ℙ.' ，sum𝕄
すべての \(n\) について（帰納法）。
Lind … \(\forall i \in \mathbb{M} . a ( i ) \in \mathbb{M} , b ( i ) \in \mathbb{M} , p ( i ) = a ( i ) \cdot b ( i ) , q ( i ) = a ( i ) \cdot a ( i ) , r ( i ) = b ( i ) \cdot b ( i ) \Longrightarrow \forall n \in \mathbb{M} . \exists t \in \mathbb{M} . ( q \sum n ) \cdot ( r \sum n ) = ( p \sum n ) \cdot ( p \sum n ) + t\) \(\blacktriangleleft\) LB ，LS ，Mstep ，Sx ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄 ，⋅𝕄 ，ℙ.' ，sum𝕄

4 コーシー・シュワルツの不等式

\(\left(\sum_{i \(\forall i \in \mathbb{M} . a ( i ) \in \mathbb{M} , b ( i ) \in \mathbb{M} , p ( i ) = a ( i ) \cdot b ( i ) , q ( i ) = a ( i ) \cdot a ( i ) , r ( i ) = b ( i ) \cdot b ( i ) \Longrightarrow \forall n \in \mathbb{M} . ( p \sum n ) \cdot ( p \sum n ) \le ( q \sum n ) \cdot ( r \sum n )\) \(\blacktriangleleft\) Lind ，Mstep ，Sx ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，sum𝕄